Theorem f1oweALT 3982

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 3771	. . . 4 |- (F:A-1-1-onto->B -> F:A-onto->B)
2		df-fo 3251	. . . . 5 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
3		freq2 2978	. . . . . . 7 |- (ran F = B -> (S Fr ran F <-> S Fr B))
4	3	biimprd 152	. . . . . 6 |- (ran F = B -> (S Fr B -> S Fr ran F))
5		df-fn 3248	. . . . . . 7 |- (F Fn A <-> (Fun F /\ dom F = A))
6		visset 1851	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. V
7	6	funimaex 3651	. . . . . . . . . . . . . . . . . . . . 21 |- (Fun F -> (F"z) e. V)
8		sseq1 2126	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (w (_ ran F <-> (F"z) (_ ran F))
9		neeq1 1627	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (w =/= (/) <-> (F"z) =/= (/)))
10	8, 9	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = (F"z) -> ((w (_ ran F /\ w =/= (/)) <-> ((F"z) (_ ran F /\ (F"z) =/= (/))))
11		raleq1 1824	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (A.f e. w -. fSu <-> A.f e. (F"z) -. fSu))
12	11	rexeqd 1830	. . . . . . . . . . . . . . . . . . . . . . . 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 628	. . . . . . . . . . . . . . . . . . . . . . 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 1900	. . . . . . . . . . . . . . . . . . . . . 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 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Fun F /\ z (_ dom F) -> (w e. z -> (F` w) e. (F"z)))
16		ne0i 2330	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1247	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun F /\ z (_ dom F) -> (E.w w e. z -> (F"z) =/= (/)))
19		n0 2333	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z =/= (/) <-> E.w w e. z)
20	18, 19	syl5ib 204	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((Fun F /\ z (_ dom F) -> (z =/= (/) -> (F"z) =/= (/)))
21	20	imp 348	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((Fun F /\ z (_ dom F) /\ z =/= (/)) -> (F"z) =/= (/))
22		imassrn 3478	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F"z) (_ ran F
23	21, 22	jctil 290	. . . . . . . . . . . . . . . . . . . . . 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 2972	. . . . . . . . . . . . . . . . . . . 20 |- (S Fr ran F <-> A.w((w (_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu))
27	25, 26	syl5ib 204	. . . . . . . . . . . . . . . . . . 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 374	. . . . . . . . . . . . . . . . 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 497	. . . . . . . . . . . . . . . 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 359	. . . . . . . . . . . . . . 15 |- ((Fun F /\ z (_ dom F) -> ((z =/= (/) /\ S Fr ran F) -> E.u e. (F"z)A.f e. (F"z) -. fSu))
32		fores 3757	. . . . . . . . . . . . . . . 16 |- ((Fun F /\ z (_ dom F) -> (F |` z):z-onto->(F"z))
33		breq1 2672	. . . . . . . . . . . . . . . . . . . . 21 |- (((F |` z)` v) = f -> (((F |` z)` v)S((F |` z)` w) <-> fS((F |` z)` w)))
34	33	notbid 613	. . . . . . . . . . . . . . . . . . . 20 |- (((F |` z)` v) = f -> (-. ((F |` z)` v)S((F |` z)` w) <-> -. fS((F |` z)` w)))
35	34	cbvfo 3961	. . . . . . . . . . . . . . . . . . 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 1702	. . . . . . . . . . . . . . . . . 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 2673	. . . . . . . . . . . . . . . . . . . . 21 |- (((F |` z)` w) = u -> (fS((F |` z)` w) <-> fSu))
38	37	notbid 613	. . . . . . . . . . . . . . . . . . . 20 |- (((F |` z)` w) = u -> (-. fS((F |` z)` w) <-> -. fSu))
39	38	ralbidv 1701	. . . . . . . . . . . . . . . . . . 19 |- (((F |` z)` w) = u -> (A.f e. (F"z) -. fS((F |` z)` w) <-> A.f e. (F"z) -. fSu))
40	39	cbvexfo 3962	. . . . . . . . . . . . . . . . . 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 530	. . . . . . . . . . . . . . . . 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 3810	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. z -> ((F |` z)` v) = (F` v))
43		fvres 3810	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. z -> ((F |` z)` w) = (F` w))
44	42, 43	breqan12rd 2683	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. z /\ v e. z) -> (((F |` z)` v)S((F |` z)` w) <-> (F` v)S(F` w)))
45		visset 1851	. . . . . . . . . . . . . . . . . . . . . 22 |- v e. V
46		visset 1851	. . . . . . . . . . . . . . . . . . . . . 22 |- w e. V
47		fveq2 3800	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = v -> (F` x) = (F` v))
48	47	breq1d 2679	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = v -> ((F` x)S(F` y) <-> (F` v)S(F` y)))
49		fveq2 3800	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = w -> (F` y) = (F` w))
50	49	breq2d 2680	. . . . . . . . . . . . . . . . . . . . . 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 2874	. . . . . . . . . . . . . . . . . . . . 21 |- (vRw <-> (F` v)S(F` w))
53	44, 52	syl6rbbr 541	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. z /\ v e. z) -> (vRw <-> ((F |` z)` v)S((F |` z)` w)))
54	53	notbid 613	. . . . . . . . . . . . . . . . . . 19 |- ((w e. z /\ v e. z) -> (-. vRw <-> -. ((F |` z)` v)S((F |` z)` w)))
55	54	ralbidva 1697	. . . . . . . . . . . . . . . . . 18 |- (w e. z -> (A.v e. z -. vRw <-> A.v e. z -. ((F |` z)` v