Theorem f1oweALT 3906

Description: Well-ordering of isomorphic relations. (This version is proved directly instead of wit the isomorphism predicate.)

Hypothesis

Ref	Expression
f1oweALT.1	|- R = {<.x, y>. | (F` x)S(F` y)}

Assertion

Ref	Expression
f1oweALT	|- (F:A-1-1-onto->B -> (S We B -> R We A))

Distinct variable groups:   x,y,S   x,F,y

Proof of Theorem f1oweALT

Step	Hyp	Ref	Expression
1		f1ofo 3695	. . . 4 |- (F:A-1-1-onto->B -> F:A-onto->B)
2		df-fo 3196	. . . . 5 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
3		freq2 2923	. . . . . . 7 |- (ran F = B -> (S Fr ran F <-> S Fr B))
4	3	biimprd 154	. . . . . 6 |- (ran F = B -> (S Fr B -> S Fr ran F))
5		df-fn 3193	. . . . . . 7 |- (F Fn A <-> (Fun F /\ dom F = A))
6		visset 1813	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. V
7	6	funimaex 3576	. . . . . . . . . . . . . . . . . . . . 21 |- (Fun F -> (F"z) e. V)
8		sseq1 2082	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (w (_ ran F <-> (F"z) (_ ran F))
9		neeq1 1590	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (w =/= (/) <-> (F"z) =/= (/)))
10	8, 9	anbi12d 628	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = (F"z) -> ((w (_ ran F /\ w =/= (/)) <-> ((F"z) (_ ran F /\ (F"z) =/= (/))))
11		raleq1 1786	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (A.f e. w -. fSu <-> A.f e. (F"z) -. fSu))
12	11	rexeqd 1792	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = (F"z) -> (E.u e. w A.f e. w -. fSu <-> E.u e. (F"z)A.f e. (F"z) -. fSu))
13	10, 12	imbi12d 626	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w = (F"z) -> (((w (_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu) <-> (((F"z) (_ ran F /\ (F"z) =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
14	13	cla4gv 1862	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F"z) e. V -> (A.w((w (_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu) -> (((F"z) (_ ran F /\ (F"z) =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
15		funfvima2 3853	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Fun F /\ z (_ dom F) -> (w e. z -> (F` w) e. (F"z)))
16		ne0i 2286	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F` w) e. (F"z) -> (F"z) =/= (/))
17	15, 16	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Fun F /\ z (_ dom F) -> (w e. z -> (F"z) =/= (/)))
18	17	19.23adv 1214	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun F /\ z (_ dom F) -> (E.w w e. z -> (F"z) =/= (/)))
19		ne0 2288	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z =/= (/) <-> E.w w e. z)
20	18, 19	syl5ib 206	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((Fun F /\ z (_ dom F) -> (z =/= (/) -> (F"z) =/= (/)))
21	20	imp 350	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((Fun F /\ z (_ dom F) /\ z =/= (/)) -> (F"z) =/= (/))
22		imassrn 3415	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F"z) (_ ran F
23	21, 22	jctil 292	. . . . . . . . . . . . . . . . . . . . . 22 |- (((Fun F /\ z (_ dom F) /\ z =/= (/)) -> ((F"z) (_ ran F /\ (F"z) =/= (/)))
24	14, 23	syl7 23	. . . . . . . . . . . . . . . . . . . . 21 |- ((F"z) e. V -> (A.w((w (_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu) -> (((Fun F /\ z (_ dom F) /\ z =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
25	7, 24	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (Fun F -> (A.w((w (_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu) -> (((Fun F /\ z (_ dom F) /\ z =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
26		df-fr 2917	. . . . . . . . . . . . . . . . . . . 20 |- (S Fr ran F <-> A.w((w (_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu))
27	25, 26	syl5ib 206	. . . . . . . . . . . . . . . . . . 19 |- (Fun F -> (S Fr ran F -> (((Fun F /\ z (_ dom F) /\ z =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
28	27	com23 32	. . . . . . . . . . . . . . . . . 18 |- (Fun F -> (((Fun F /\ z (_ dom F) /\ z =/= (/)) -> (S Fr ran F -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
29	28	exp3a 375	. . . . . . . . . . . . . . . . 17 |- (Fun F -> ((Fun F /\ z (_ dom F) -> (z =/= (/) -> (S Fr ran F -> E.u e. (F"z)A.f e. (F"z) -. fSu))))
30	29	anabsi5 495	. . . . . . . . . . . . . . . 16 |- ((Fun F /\ z (_ dom F) -> (z =/= (/) -> (S Fr ran F -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
31	30	imp3a 361	. . . . . . . . . . . . . . 15 |- ((Fun F /\ z (_ dom F) -> ((z =/= (/) /\ S Fr ran F) -> E.u e. (F"z)A.f e. (F"z) -. fSu))
32		fores 3681	. . . . . . . . . . . . . . . 16 |- ((Fun F /\ z (_ dom F) -> (F |` z):z-onto->(F"z))
33		breq1 2622	. . . . . . . . . . . . . . . . . . . . 21 |- (((F |` z)` v) = f -> (((F |` z)` v)S((F |` z)` w) <-> fS((F |` z)` w)))
34	33	negbid 611	. . . . . . . . . . . . . . . . . . . 20 |- (((F |` z)` v) = f -> (-. ((F |` z)` v)S((F |` z)` w) <-> -. fS((F |` z)` w)))
35	34	cbvfo 3885	. . . . . . . . . . . . . . . . . . 19 |- ((F |` z):z-onto->(F"z) -> (A.v e. z -. ((F |` z)` v)S((F |` z)` w) <-> A.f e. (F"z) -. fS((F |` z)` w)))
36	35	rexbidv 1664	. . . . . . . . . . . . . . . . . 18 |- ((F |` z):z-onto->(F"z) -> (E.w e. z A.v e. z -. ((F |` z)` v)S((F |` z)` w) <-> E.w e. z A.f e. (F"z) -. fS((F |` z)` w)))
37		breq2 2623	. . . . . . . . . . . . . . . . . . . . 21 |- (((F |` z)` w) = u -> (fS((F |` z)` w) <-> fSu))
38	37	negbid 611	. . . . . . . . . . . . . . . . . . . 20 |- (((F |` z)` w) = u -> (-. fS((F |` z)` w) <-> -. fSu))
39	38	ralbidv 1663	. . . . . . . . . . . . . . . . . . 19 |- (((F |` z)` w) = u -> (A.f e. (F"z) -. fS((F |` z)` w) <-> A.f e. (F"z) -. fSu))
40	39	cbvexfo 3886	. . . . . . . . . . . . . . . . . 18 |- ((F |` z):z-onto->(F"z) -> (E.w e. z A.f e. (F"z) -. fS((F |` z)` w) <-> E.u e. (F"z)A.f e. (F"z) -. fSu))
41	36, 40	bitrd 528	. . . . . . . . . . . . . . . . 17 |- ((F |` z):z-onto->(F"z) -> (E.w e. z A.v e. z -. ((F |` z)` v)S((F |` z)` w) <-> E.u e. (F"z)A.f e. (F"z) -. fSu))
42		fvres 3734	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. z -> ((F |` z)` v) = (F` v))
43		fvres 3734	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. z -> ((F |` z)` w) = (F` w))
44	42, 43	breqan12rd 2633	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. z /\ v e. z) -> (((F |` z)` v)S((F |` z)` w) <-> (F` v)S(F` w)))
45		visset 1813	. . . . . . . . . . . . . . . . . . . . . 22 |- v e. V
46		visset 1813	. . . . . . . . . . . . . . . . . . . . . 22 |- w e. V
47		fveq2 3724	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = v -> (F` x) = (F` v))
48	47	breq1d 2629	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = v -> ((F` x)S(F` y) <-> (F` v)S(F` y)))
49		fveq2 3724	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = w -> (F` y) = (F` w))
50	49	breq2d 2630	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = w -> ((F` v)S(F` y) <-> (F` v)S(F` w)))
51		f1oweALT.1	. . . . . . . . . . . . . . . . . . . . . 22 |- R = {<.x, y>. | (F` x)S(F` y)}
52	45, 46, 48, 50, 51	brab 2821	. . . . . . . . . . . . . . . . . . . . 21 |- (vRw <-> (F` v)S(F` w))
53	44, 52	syl6rbbr 539	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. z /\ v e. z) -> (vRw <-> ((F |` z)` v)S((F |` z)` w)))
54	53	negbid 611	. . . . . . . . . . . . . . . . . . 19 |- ((w e. z /\ v e. z) -> (-. vRw <-> -. ((F |` z)` v)S((F |` z)` w)))
55	54	ralbidva 1659	. . . . . . . . . . . . . . . . . 18 |- (w e. z -> (A.v e. z -. vRw <-> A.v e. z -. ((F |` z)` v