Theorem f1oweOLD 2944

Description: Well-ordering of isomorphic relations.

Hypothesis

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

Assertion

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

Distinct variable group(s):   x,y,S   x,F,y

Proof of Theorem f1oweOLD

Step	Hyp	Ref	Expression
1		df-f1o 2437	. . . . 5 |- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
2	1	pm3.27bd 263	. . . 4 |- (F:A-1-1-onto->B -> F:A-onto->B)
3		df-fo 2436	. . . . 5 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
4		freq2 2175	. . . . . . 7 |- (ran F = B -> (S Fr ran F <-> S Fr B))
5	4	biimprd 136	. . . . . 6 |- (ran F = B -> (S Fr B -> S Fr ran F))
6		df-fn 2433	. . . . . . 7 |- (F Fn A <-> (Fun F /\ dom F = A))
7		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. V
8	7	funimaex 2716	. . . . . . . . . . . . . . . . . . . . 21 |- (Fun F -> (F"z) e. V)
9		sseq1 1521	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (w (_ ran F <-> (F"z) (_ ran F))
10		cleq1 1107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (F"z) -> (w = (/) <-> (F"z) = (/)))
11	10	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (-. w = (/) <-> -. (F"z) = (/)))
12	9, 11	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = (F"z) -> ((w (_ ran F /\ -. w = (/)) <-> ((F"z) (_ ran F /\ -. (F"z) = (/))))
13		raleq 1324	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (A.f e. w -. fSu <-> A.f e. (F"z) -. fSu))
14	13	rexeqd 1328	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = (F"z) -> (E.u e. w A.f e. w -. fSu <-> E.u e. (F"z)A.f e. (F"z) -. fSu))
15	12, 14	imbi12d 474	. . . . . . . . . . . . . . . . . . . . . . 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)))
16	15	cla4gv 1396	. . . . . . . . . . . . . . . . . . . . . 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)))
17		funfvima2 2905	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Fun F /\ z (_ dom F) -> (w e. z -> (F` w) e. (F"z)))
18		n0i 1712	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F` w) e. (F"z) -> -. (F"z) = (/))
19	17, 18	syl6 23	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Fun F /\ z (_ dom F) -> (w e. z -> -. (F"z) = (/)))
20	19	19.23adv 954	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun F /\ z (_ dom F) -> (E.w w e. z -> -. (F"z) = (/)))
21		n0 1714	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (-. z = (/) <-> E.w w e. z)
22	20, 21	syl5ib 181	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((Fun F /\ z (_ dom F) -> (-. z = (/) -> -. (F"z) = (/)))
23	22	imp 277	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((Fun F /\ z (_ dom F) /\ -. z = (/)) -> -. (F"z) = (/))
24		imassrn 2611	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F"z) (_ ran F
25	23, 24	jctil 240	. . . . . . . . . . . . . . . . . . . . . 22 |- (((Fun F /\ z (_ dom F) /\ -. z = (/)) -> ((F"z) (_ ran F /\ -. (F"z) = (/)))
26	16, 25	syl7 24	. . . . . . . . . . . . . . . . . . . . 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)))
27	8, 26	syl 12	. . . . . . . . . . . . . . . . . . . 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)))
28		df-fr 2169	. . . . . . . . . . . . . . . . . . . 20 |- (S Fr ran F <-> A.w((w (_ ran F /\ -. w = (/)) -> E.u e. w A.f e. w -. fSu))
29	27, 28	syl5ib 181	. . . . . . . . . . . . . . . . . . 19 |- (Fun F -> (S Fr ran F -> (((Fun F /\ z (_ dom F) /\ -. z = (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
30	29	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)))
31	30	exp3a 292	. . . . . . . . . . . . . . . . 17 |- (Fun F -> ((Fun F /\ z (_ dom F) -> (-. z = (/) -> (S Fr ran F -> E.u e. (F"z)A.f e. (F"z) -. fSu))))
32	31	anabsi5 377	. . . . . . . . . . . . . . . 16 |- ((Fun F /\ z (_ dom F) -> (-. z = (/) -> (S Fr ran F -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
33	32	imp3a 279	. . . . . . . . . . . . . . 15 |- ((Fun F /\ z (_ dom F) -> ((-. z = (/) /\ S Fr ran F) -> E.u e. (F"z)A.f e. (F"z) -. fSu))
34		fores 2794	. . . . . . . . . . . . . . . 16 |- ((Fun F /\ z (_ dom F) -> (F |` z):z-onto->(F"z))
35		breq1 2065	. . . . . . . . . . . . . . . . . . . . 21 |- (((F |` z)` v) = f -> (((F |` z)` v)S((F |` z)` w) <-> fS((F |` z)` w)))
36	35	negbid 463	. . . . . . . . . . . . . . . . . . . 20 |- (((F |` z)` v) = f -> (-. ((F |` z)` v)S((F |` z)` w) <-> -. fS((F |` z)` w)))
37	36	cbvfo 2923	. . . . . . . . . . . . . . . . . . 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)))
38	37	birexdv 1220	. . . . . . . . . . . . . . . . . 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)))
39		breq2 2066	. . . . . . . . . . . . . . . . . . . . 21 |- (((F |` z)` w) = u -> (fS((F |` z)` w) <-> fSu))
40	39	negbid 463	. . . . . . . . . . . . . . . . . . . 20 |- (((F |` z)` w) = u -> (-. fS((F |` z)` w) <-> -. fSu))
41	40	biraldv 1219	. . . . . . . . . . . . . . . . . . 19 |- (((F |` z)` w) = u -> (A.f e. (F"z) -. fS((F |` z)` w) <-> A.f e. (F"z) -. fSu))
42	41	cbvexfo 2924	. . . . . . . . . . . . . . . . . 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))
43	38, 42	bitrd 406	. . . . . . . . . . . . . . . . 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))
44		fvres 2840	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. z -> ((F |` z)` v) = (F` v))
45		fvres 2840	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. z -> ((F |` z)` w) = (F` w))
46	44, 45	breqan12rd 2075	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. z /\ v e. z) -> (((F |` z)` v)S((F |` z)` w) <-> (F` v)S(F` w)))
47		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 |- v e. V
48		visset 1350	. . . . . . . . . . . . . . . . . . . . . 22 |- w e. V
49		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = v -> (F` x) = (F` v))
50	49	breq1d 2071	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = v -> ((F` x)S(F` y) <-> (F` v)S(F` y)))
51		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = w -> (F` y) = (F` w))
52	51	breq2d 2072	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = w -> ((F` v)S(F` y) <-> (F` v)S(F` w)))
53		f1oweOLD.1	. . . . . . . . . . . . . . . . . . . . . 22 |- R = {<.x, y>. | (F` x)S(F` y)}
54	47, 48, 50, 52, 53	brab 2118	. . . . . . . . . . . . . . . . . . . . 21 |- (vRw <-> (F` v)S(F` w))
55	46, 54	syl6rbbr 417	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. z /\ v e. z) -> (vRw <-> ((F |` z)` v)S((F |` z)` w)))
56	55	negbid 463	. . . . . . . . . . . . . . . . . . 19 |- ((w e. z /\ v e. z) -> (-. vRw <-> -. ((F |` z)` v)S((F |` z)` w)))
57	56	biraldva 1215	. . . . . . . . . . . . . . . . . 18 |- (w e. z -> (A.v e. z -. v