Theorem isofrlem 3907

Description: Lemma for isofr 3908.

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 3899	. . . . . . 7 |- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
2		f1ofun 3697	. . . . . . 7 |- (H:A-1-1-onto->B -> Fun H)
3		visset 1816	. . . . . . . . 9 |- x e. V
4	3	funimaex 3582	. . . . . . . 8 |- (Fun H -> (H"x) e. V)
5		sseq1 2085	. . . . . . . . . . 11 |- (z = (H"x) -> (z (_ B <-> (H"x) (_ B))
6		neeq1 1593	. . . . . . . . . . 11 |- (z = (H"x) -> (z =/= (/) <-> (H"x) =/= (/)))
7	5, 6	anbi12d 630	. . . . . . . . . 10 |- (z = (H"x) -> ((z (_ B /\ z =/= (/)) <-> ((H"x) (_ B /\ (H"x) =/= (/))))
8		ineq1 2213	. . . . . . . . . . . 12 |- (z = (H"x) -> (z i^i (`'S"{w})) = ((H"x) i^i (`'S"{w})))
9	8	eqeq1d 1486	. . . . . . . . . . 11 |- (z = (H"x) -> ((z i^i (`'S"{w})) = (/) <-> ((H"x) i^i (`'S"{w})) = (/)))
10	9	rexeqd 1795	. . . . . . . . . 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 628	. . . . . . . . 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 1865	. . . . . . . 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 3437	. . . . . 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 3696	. . . . . . . 8 |- (H:A-1-1-onto->B -> H Fn A)
18		ssel 2066	. . . . . . . . . . . . 13 |- (x (_ A -> (y e. x -> y e. A))
19		funfvima 3858	. . . . . . . . . . . . . . . 16 |- ((Fun H /\ y e. dom H) -> (y e. x -> (H` y) e. (H"x)))
20	19	funfni 3594	. . . . . . . . . . . . . . 15 |- ((H Fn A /\ y e. A) -> (y e. x -> (H` y) e. (H"x)))
21		ne0i 2289	. . . . . . . . . . . . . . 15 |- ((H` y) e. (H"x) -> (H"x) =/= (/))
22	20, 21	syl6 22	. . . . . . . . . . . . . 14 |- ((H Fn A /\ y e. A) -> (y e. x -> (H"x) =/= (/)))
23	22	ex 373	. . . . . . . . . . . . 13 |- (H Fn A -> (y e. A -> (y e. x -> (H"x) =/= (/))))
24	18, 23	sylan9r 471	. . . . . . . . . . . 12 |- ((H Fn A /\ x (_ A) -> (y e. x -> (y e. x -> (H"x) =/= (/))))
25	24	pm2.43d 65	. . . . . . . . . . 11 |- ((H Fn A /\ x (_ A) -> (y e. x -> (H"x) =/= (/)))
26	25	19.23adv 1216	. . . . . . . . . 10 |- ((H Fn A /\ x (_ A) -> (E.y y e. x -> (H"x) =/= (/)))
27		ne0 2292	. . . . . . . . . 10 |- (x =/= (/) <-> E.y y e. x)
28	26, 27	syl5ib 206	. . . . . . . . 9 |- ((H Fn A /\ x (_ A) -> (x =/= (/) -> (H"x) =/= (/)))
29	28	expimpd 375	. . . . . . . 8 |- (H Fn A -> ((x (_ A /\ x =/= (/)) -> (H"x) =/= (/)))
30	17, 29	syl 10	. . . . . . 7 |- (H:A-1-1-onto->B -> ((x (_ A /\ x =/= (/)) -> (H"x) =/= (/)))
31		f1ofo 3701	. . . . . . . 8 |- (H:A-1-1-onto->B -> H:A-onto->B)
32		imassrn 3421	. . . . . . . . 9 |- (H"x) (_ ran H
33		forn 3680	. . . . . . . . . 10 |- (H:A-onto->B -> ran H = B)
34	33	sseq2d 2092	. . . . . . . . 9 |- (H:A-onto->B -> ((H"x) (_ ran H <-> (H"x) (_ B))
35	32, 34	mpbii 193	. . . . . . . 8 |- (H:A-onto->B -> (H"x) (_ B)
36	31, 35	syl 10	. . . . . . 7 |- (H:A-1-1-onto->B -> (H"x) (_ B)
37	30, 36	jctild 603	. . . . . 6 |- (H:A-1-1-onto->B -> ((x (_ A /\ x =/= (/)) -> ((H"x) (_ B /\ (H"x) =/= (/))))
38	1, 37	syl 10	. . . . 5 |- (H Isom R, S (A, B) -> ((x (_ A /\ x =/= (/)) -> ((H"x) (_ B /\ (H"x) =/= (/))))
39	16, 38	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})) = (/))))
40		fvelima 3770	. . . . . . . . . . 11 |- ((Fun H /\ w e. (H"x)) -> E.y e. x (H` y) = w)
41	1	adantr 391	. . . . . . . . . . . 12 |- ((H Isom R, S (A, B) /\ x (_ A) -> H:A-1-1-onto->B)
42	41, 2	syl 10	. . . . . . . . . . 11 |- ((H Isom R, S (A, B) /\ x (_ A) -> Fun H)
43		pm3.26 319	. . . . . . . . . . 11 |- ((w e. (H"x) /\ ((H"x) i^i (`'S"{w})) = (/)) -> w e. (H"x))
44	40, 42, 43	syl2an 456	. . . . . . . . . 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)
45		isomin 3905	. . . . . . . . . . . . . . . . . . 19 |- ((H Isom R, S (A, B) /\ (x (_ A /\ y e. A)) -> ((x i^i (`'R"{y})) = (/) <-> ((H"x) i^i (`'S"{(H` y)})) = (/)))
46	18	imdistani 445	. . . . . . . . . . . . . . . . . . 19 |- ((x (_ A /\ y e. x) -> (x (_ A /\ y e. A))
47	45, 46	sylan2 453	. . . . . . . . . . . . . . . . . 18 |- ((H Isom R, S (A, B) /\ (x (_ A /\ y e. x)) -> ((x i^i (`'R"{y})) = (/) <-> ((H"x) i^i (`'S"{(H` y)})) = (/)))
48		sneq 2421	. . . . . . . . . . . . . . . . . . . . 21 |- ((H` y) = w -> {(H` y)} = {w})
49	48	imaeq2d 3410	. . . . . . . . . . . . . . . . . . . 20 |- ((H` y) = w -> (`'S"{(H` y)}) = (`'S"{w}))
50	49	ineq2d 2220	. . . . . . . . . . . . . . . . . . 19 |- ((H` y) = w -> ((H"x) i^i (`'S"{(H` y)})) = ((H"x) i^i (`'S"{w})))
51	50	eqeq1d 1486	. . . . . . . . . . . . . . . . . 18 |- ((H` y) = w -> (((H"x) i^i (`'S"{(H` y)})) = (/) <-> ((H"x) i^i (`'S"{w})) = (/)))
52	47, 51	sylan9bb 542	. . . . . . . . . . . . . . . . 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})) = (/)))
53		pm3.27 323	. . . . . . . . . . . . . . . . 17 |- ((w e. (H"x) /\ ((H"x) i^i (`'S"{w})) = (/)) -> ((H"x) i^i (`'S"{w})) = (/))
54	52, 53	syl5bir 210	. . . . . . . . . . . . . . . 16 |- (((H Isom R, S (A, B) /\ (x (_ A /\ y e. x)) /\ (H` y) = w) -> ((w e. (H"x) /\ ((H"x) i^i (`'