Theorem isofrlem 3892

Description: Lemma for isofr 3893.

Assertion

Ref	Expression
isofrlem	|- (H Isom R, S (A, B) -> (S Fr B -> R Fr A))

Proof of Theorem isofrlem

Step	Hyp	Ref	Expression
1		isof1o 3884	. . . . . . 7 |- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
2		f1ofun 3682	. . . . . . 7 |- (H:A-1-1-onto->B -> Fun H)
3		visset 1809	. . . . . . . . 9 |- x e. V
4	3	funimaex 3568	. . . . . . . 8 |- (Fun H -> (H"x) e. V)
5		sseq1 2078	. . . . . . . . . . 11 |- (z = (H"x) -> (z (_ B <-> (H"x) (_ B))
6		neeq1 1587	. . . . . . . . . . 11 |- (z = (H"x) -> (z =/= (/) <-> (H"x) =/= (/)))
7	5, 6	anbi12d 627	. . . . . . . . . 10 |- (z = (H"x) -> ((z (_ B /\ z =/= (/)) <-> ((H"x) (_ B /\ (H"x) =/= (/))))
8		ineq1 2206	. . . . . . . . . . . 12 |- (z = (H"x) -> (z i^i (`'S"{w})) = ((H"x) i^i (`'S"{w})))
9	8	eqeq1d 1480	. . . . . . . . . . 11 |- (z = (H"x) -> ((z i^i (`'S"{w})) = (/) <-> ((H"x) i^i (`'S"{w})) = (/)))
10	9	rexeqd 1789	. . . . . . . . . 10 |- (z = (H"x) -> (E.w e. z (z i^i (`'S"{w})) = (/) <-> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/)))
11	7, 10	imbi12d 625	. . . . . . . . 9 |- (z = (H"x) -> (((z (_ B /\ z =/= (/)) -> E.w e. z (z i^i (`'S"{w})) = (/)) <-> (((H"x) (_ B /\ (H"x) =/= (/)) -> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/))))
12	11	cla4gv 1858	. . . . . . . 8 |- ((H"x) e. V -> (A.z((z (_ B /\ z =/= (/)) -> E.w e. z (z i^i (`'S"{w})) = (/)) -> (((H"x) (_ B /\ (H"x) =/= (/)) -> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/))))
13	4, 12	syl 10	. . . . . . 7 |- (Fun H -> (A.z((z (_ B /\ z =/= (/)) -> E.w e. z (z i^i (`'S"{w})) = (/)) -> (((H"x) (_ B /\ (H"x) =/= (/)) -> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/))))
14	1, 2, 13	3syl 20	. . . . . 6 |- (H Isom R, S (A, B) -> (A.z((z (_ B /\ z =/= (/)) -> E.w e. z (z i^i (`'S"{w})) = (/)) -> (((H"x) (_ B /\ (H"x) =/= (/)) -> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/))))
15		dffr3 3423	. . . . . 6 |- (S Fr B <-> A.z((z (_ B /\ z =/= (/)) -> E.w e. z (z i^i (`'S"{w})) = (/)))
16	14, 15	syl5ib 206	. . . . 5 |- (H Isom R, S (A, B) -> (S Fr B -> (((H"x) (_ B /\ (H"x) =/= (/)) -> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/))))
17		f1ofn 3681	. . . . . . . 8 |- (H:A-1-1-onto->B -> H Fn A)
18		ssel 2059	. . . . . . . . . . . . . 14 |- (x (_ A -> (y e. x -> y e. A))
19		funfvima 3843	. . . . . . . . . . . . . . . . 17 |- ((Fun H /\ y e. dom H) -> (y e. x -> (H` y) e. (H"x)))
20	19	funfni 3580	. . . . . . . . . . . . . . . 16 |- ((H Fn A /\ y e. A) -> (y e. x -> (H` y) e. (H"x)))
21		ne0i 2282	. . . . . . . . . . . . . . . 16 |- ((H` y) e. (H"x) -> (H"x) =/= (/))
22	20, 21	syl6 22	. . . . . . . . . . . . . . 15 |- ((H Fn A /\ y e. A) -> (y e. x -> (H"x) =/= (/)))
23	22	ex 373	. . . . . . . . . . . . . 14 |- (H Fn A -> (y e. A -> (y e. x -> (H"x) =/= (/))))
24	18, 23	sylan9r 469	. . . . . . . . . . . . 13 |- ((H Fn A /\ x (_ A) -> (y e. x -> (y e. x -> (H"x) =/= (/))))
25	24	pm2.43d 65	. . . . . . . . . . . 12 |- ((H Fn A /\ x (_ A) -> (y e. x -> (H"x) =/= (/)))
26	25	19.23adv 1212	. . . . . . . . . . 11 |- ((H Fn A /\ x (_ A) -> (E.y y e. x -> (H"x) =/= (/)))
27		ne0 2284	. . . . . . . . . . 11 |- (x =/= (/) <-> E.y y e. x)
28	26, 27	syl5ib 206	. . . . . . . . . 10 |- ((H Fn A /\ x (_ A) -> (x =/= (/) -> (H"x) =/= (/)))
29	28	ex 373	. . . . . . . . 9 |- (H Fn A -> (x (_ A -> (x =/= (/) -> (H"x) =/= (/))))
30	29	imp3a 361	. . . . . . . 8 |- (H Fn A -> ((x (_ A /\ x =/= (/)) -> (H"x) =/= (/)))
31	17, 30	syl 10	. . . . . . 7 |- (H:A-1-1-onto->B -> ((x (_ A /\ x =/= (/)) -> (H"x) =/= (/)))
32		f1ofo 3686	. . . . . . . 8 |- (H:A-1-1-onto->B -> H:A-onto->B)
33		imassrn 3407	. . . . . . . . 9 |- (H"x) (_ ran H
34		forn 3665	. . . . . . . . . 10 |- (H:A-onto->B -> ran H = B)
35	34	sseq2d 2085	. . . . . . . . 9 |- (H:A-onto->B -> ((H"x) (_ ran H <-> (H"x) (_ B))
36	33, 35	mpbii 193	. . . . . . . 8 |- (H:A-onto->B -> (H"x) (_ B)
37	32, 36	syl 10	. . . . . . 7 |- (H:A-1-1-onto->B -> (H"x) (_ B)
38	31, 37	jctild 600	. . . . . 6 |- (H:A-1-1-onto->B -> ((x (_ A /\ x =/= (/)) -> ((H"x) (_ B /\ (H"x) =/= (/))))
39	1, 38	syl 10	. . . . 5 |- (H Isom R, S (A, B) -> ((x (_ A /\ x =/= (/)) -> ((H"x) (_ B /\ (H"x) =/= (/))))
40	16, 39	syl5d 55	. . . 4 |- (H Isom R, S (A, B) -> (S Fr B -> ((x (_ A /\ x =/= (/)) -> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/))))
41		fvelima 3755	. . . . . . . . . . 11 |- ((Fun H /\ w e. (H"x)) -> E.y e. x (H` y) = w)
42	1	adantr 389	. . . . . . . . . . . 12 |- ((H Isom R, S (A, B) /\ x (_ A) -> H:A-1-1-onto->B)
43	42, 2	syl 10	. . . . . . . . . . 11 |- ((H Isom R, S (A, B) /\ x (_ A) -> Fun H)
44		pm3.26 319	. . . . . . . . . . 11 |- ((w e. (H"x) /\ ((H"x) i^i (`'S"{w})) = (/)) -> w e. (H"x))
45	41, 43, 44	syl2an 454	. . . . . . . . . 10 |- (((H Isom R, S (A, B) /\ x (_ A) /\ (w e. (H"x) /\ ((H"x) i^i (`'S"{w})) = (/))) -> E.y e. x (H` y) = w)
46		isomin 3890	. . . . . . . . . . . . . . . . . . 19 |- ((H Isom R, S (A, B) /\ (x (_ A /\ y e. A)) -> ((x i^i (`'R"{y})) = (/) <-> ((H"x) i^i (`'S"{(H` y)})) = (/)))
47	18	imdistani 443	. . . . . . . . . . . . . . . . . . 19 |- ((x (_ A /\ y e. x) -> (x (_ A /\ y e. A))
48	46, 47	sylan2 451	. . . . . . . . . . . . . . . . . 18 |- ((H Isom R, S (A, B) /\ (x (_ A /\ y e. x)) -> ((x i^i (`'R"{y})) = (/) <-> ((H"x) i^i (`'S"{(H` y)})) = (/)))
49		sneq 2413	. . . . . . . . . . . . . . . . . . . . 21 |- ((H` y) = w -> {(H` y)} = {w})
50	49	imaeq2d 3396	. . . . . . . . . . . . . . . . . . . 20 |- ((H` y) = w -> (`'S"{(H` y)}) = (`'S"{w}))
51	50	ineq2d 2213	. . . . . . . . . . . . . . . . . . 19 |- ((H` y) = w -> ((H"x) i^i (`'S"{(H` y)})) = ((H"x) i^i (`'S"{w})))
52	51	eqeq1d 1480	. . . . . . . . . . . . . . . . . 18 |- ((H` y) = w -> (((H"x) i^i (`'S"{(H` y)})) = (/) <-> ((H"x) i^i (`'S"{w})) = (/)))
53	48, 52	sylan9bb 539	. . . . . . . . . . . . . . . . 17 |- (((H Isom R, S (A, B) /\ (x (_ A /\ y e. x)) /\ (H` y) = w) -> ((x i^i (`'R"{y})) = (/) <-> ((H"x) i^i (`'S"{w})) = (/)))
54		pm3.27 323	. . . . . . . . . . . . . . . . 17 |- ((w e. (H"x) /\ ((H"x) i^i (`'S"{w})) = (/)) -> ((H"x) i^i (`'S"{w})) = (/))
55	53, 54	syl5bir 210	. . . . . . . . . . . . . . . 16 |- (((H Isom R, S (A, B) /\ (x (_ A /\ y e. x)