Theorem isofrlem 2939

Description: Lemma for isofr 2940.

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 2931	. . . . . . 7 |- (H Isom R, S (A, B) -> H:A-1-1-onto->B)
2		f1ofun 2802	. . . . . . 7 |- (H:A-1-1-onto->B -> Fun H)
3		visset 1350	. . . . . . . . 9 |- x e. V
4	3	funimaex 2716	. . . . . . . 8 |- (Fun H -> (H"x) e. V)
5		sseq1 1521	. . . . . . . . . . 11 |- (z = (H"x) -> (z (_ B <-> (H"x) (_ B))
6		cleq1 1107	. . . . . . . . . . . 12 |- (z = (H"x) -> (z = (/) <-> (H"x) = (/)))
7	6	negbid 463	. . . . . . . . . . 11 |- (z = (H"x) -> (-. z = (/) <-> -. (H"x) = (/)))
8	5, 7	anbi12d 476	. . . . . . . . . 10 |- (z = (H"x) -> ((z (_ B /\ -. z = (/)) <-> ((H"x) (_ B /\ -. (H"x) = (/))))
9		ineq1 1638	. . . . . . . . . . . 12 |- (z = (H"x) -> (z i^i (`'S"{w})) = ((H"x) i^i (`'S"{w})))
10	9	cleq1d 1109	. . . . . . . . . . 11 |- (z = (H"x) -> ((z i^i (`'S"{w})) = (/) <-> ((H"x) i^i (`'S"{w})) = (/)))
11	10	rexeqd 1328	. . . . . . . . . 10 |- (z = (H"x) -> (E.w e. z (z i^i (`'S"{w})) = (/) <-> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/)))
12	8, 11	imbi12d 474	. . . . . . . . 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})) = (/))))
13	12	cla4gv 1396	. . . . . . . 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})) = (/))))
14	4, 13	syl 12	. . . . . . 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})) = (/))))
15	1, 2, 14	3syl 21	. . . . . 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})) = (/))))
16		dffr3 2620	. . . . . 6 |- (S Fr B <-> A.z((z (_ B /\ -. z = (/)) -> E.w e. z (z i^i (`'S"{w})) = (/)))
17	15, 16	syl5ib 181	. . . . 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})) = (/))))
18		f1ofo 2806	. . . . . . . . 9 |- (H:A-1-1-onto->B -> H:A-onto->B)
19		imassrn 2611	. . . . . . . . . 10 |- (H"x) (_ ran H
20		forn 2789	. . . . . . . . . . 11 |- (H:A-onto->B -> ran H = B)
21	20	sseq2d 1528	. . . . . . . . . 10 |- (H:A-onto->B -> ((H"x) (_ ran H <-> (H"x) (_ B))
22	19, 21	mpbii 168	. . . . . . . . 9 |- (H:A-onto->B -> (H"x) (_ B)
23	18, 22	syl 12	. . . . . . . 8 |- (H:A-1-1-onto->B -> (H"x) (_ B)
24	23	a1d 14	. . . . . . 7 |- (H:A-1-1-onto->B -> ((x (_ A /\ -. x = (/)) -> (H"x) (_ B))
25		f1ofn 2801	. . . . . . . 8 |- (H:A-1-1-onto->B -> H Fn A)
26		ssel 1502	. . . . . . . . . . . . . 14 |- (x (_ A -> (y e. x -> y e. A))
27		funfvima 2904	. . . . . . . . . . . . . . . . 17 |- ((Fun H /\ y e. dom H) -> (y e. x -> (H` y) e. (H"x)))
28	27	funfni 2724	. . . . . . . . . . . . . . . 16 |- ((H Fn A /\ y e. A) -> (y e. x -> (H` y) e. (H"x)))
29		n0i 1712	. . . . . . . . . . . . . . . 16 |- ((H` y) e. (H"x) -> -. (H"x) = (/))
30	28, 29	syl6 23	. . . . . . . . . . . . . . 15 |- ((H Fn A /\ y e. A) -> (y e. x -> -. (H"x) = (/)))
31	30	exp 291	. . . . . . . . . . . . . 14 |- (H Fn A -> (y e. A -> (y e. x -> -. (H"x) = (/))))
32	26, 31	sylan9r 360	. . . . . . . . . . . . 13 |- ((H Fn A /\ x (_ A) -> (y e. x -> (y e. x -> -. (H"x) = (/))))
33	32	pm2.43d 59	. . . . . . . . . . . 12 |- ((H Fn A /\ x (_ A) -> (y e. x -> -. (H"x) = (/)))
34	33	19.23adv 954	. . . . . . . . . . 11 |- ((H Fn A /\ x (_ A) -> (E.y y e. x -> -. (H"x) = (/)))
35		n0 1714	. . . . . . . . . . 11 |- (-. x = (/) <-> E.y y e. x)
36	34, 35	syl5ib 181	. . . . . . . . . 10 |- ((H Fn A /\ x (_ A) -> (-. x = (/) -> -. (H"x) = (/)))
37	36	exp 291	. . . . . . . . 9 |- (H Fn A -> (x (_ A -> (-. x = (/) -> -. (H"x) = (/))))
38	37	imp3a 279	. . . . . . . 8 |- (H Fn A -> ((x (_ A /\ -. x = (/)) -> -. (H"x) = (/)))
39	25, 38	syl 12	. . . . . . 7 |- (H:A-1-1-onto->B -> ((x (_ A /\ -. x = (/)) -> -. (H"x) = (/)))
40	24, 39	jcad 455	. . . . . 6 |- (H:A-1-1-onto->B -> ((x (_ A /\ -. x = (/)) -> ((H"x) (_ B /\ -. (H"x) = (/))))
41	1, 40	syl 12	. . . . 5 |- (H Isom R, S (A, B) -> ((x (_ A /\ -. x = (/)) -> ((H"x) (_ B /\ -. (H"x) = (/))))
42	17, 41	syl5d 53	. . . 4 |- (H Isom R, S (A, B) -> (S Fr B -> ((x (_ A /\ -. x = (/)) -> E.w e. (H"x)((H"x) i^i (`'S"{w})) = (/))))
43		fvelima 2859	. . . . . . . . . . 11 |- ((Fun H /\ w e. (H"x)) -> E.y e. x (H` y) = w)
44	1	adantr 306	. . . . . . . . . . . 12 |- ((H Isom R, S (A, B) /\ x (_ A) -> H:A-1-1-onto->B)
45	44, 2	syl 12	. . . . . . . . . . 11 |- ((H Isom R, S (A, B) /\ x (_ A) -> Fun H)
46		pm3.26 256	. . . . . . . . . . 11 |- ((w e. (H"x) /\ ((H"x) i^i (`'S"{w})) = (/)) -> w e. (H"x))
47	43, 45, 46	syl2an 349	. . . . . . . . . 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)
48		isomin 2937	. . . . . . . . . . . . . . . . . . 19 |- ((H Isom R, S (A, B) /\ (x (_ A /\ y e. A)) -> ((x i^i (`'R"{y})) = (/) <-> ((H"x) i^i (`'S"{(H` y)})) = (/)))
49	26	imdistani 340	. . . . . . . . . . . . . . . . . . 19 |- ((x (_ A /\ y e. x) -> (x (_ A /\ y e. A))
50	48, 49	sylan2 346	. . . . . . . . . . . . . . . . . 18 |- ((H Isom R, S (A, B) /\ (x (_ A /\ y e. x)) -> ((x i^i (`'R"{y})) = (/) <-> ((H"x) i^i (`'S"{(H` y)})) = (/)))
51		sneq 1816	. . . . . . . . . . . . . . . . . . . . 21 |- ((H` y) = w -> {(H` y)} = {w})
52		imaeq2 2603	. . . . . . . . . . . . . . . . . . . . 21 |- ({(H` y)} = {w} -> (`'S"{(H` y)}) = (`'S"{w}))
53	51, 52	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- ((H` y) = w -> (`'S"{(H` y)}) = (`'S"{w}))
54	53	ineq2d 1645	. . . . . . . . . . . . . . . . . . 19 |- ((H` y) = w -> ((H"x) i^i (`'S"{(H` y)})) = ((H"x) i^i (`'S"{w})))
55	54	cleq1d 1109	. . . . . . . . . . . . . . . . . 18 |- ((H` y) = w -> (((H"x) i^i (`'S"{(H` y)})) = (/) <-> ((H"x) i^i (`'S"{w})) = (/)))
56	50, 55	sylan9bb 418	. . . . . . . . . . . . . . . . 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})) = (/)))
57		pm3.27 260	. . . . . . . . . . . . . . . . 17 |- ((w e. (H"x) /\ ((