Theorem f1oweALT 4883

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 4643	. . . 4 |- (F:A-1-1-onto->B -> F:A-onto->B)
2		df-fo 4012	. . . . 5 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
3		freq2 3633	. . . . . . 7 |- (ran F = B -> (S Fr ran F <-> S Fr B))
4	3	biimprd 171	. . . . . 6 |- (ran F = B -> (S Fr B -> S Fr ran F))
5		df-fn 4009	. . . . . . 7 |- (F Fn A <-> (Fun F /\ dom F = A))
6		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- z e. _V
7	6	funimaex 4496	. . . . . . . . . . . . . . . . . . . . 21 |- (Fun F -> (F"z) e. _V)
8		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (w C_ ran F <-> (F"z) C_ ran F))
9		neeq1 2024	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (w =/= (/) <-> (F"z) =/= (/)))
10	8, 9	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = (F"z) -> ((w C_ ran F /\ w =/= (/)) <-> ((F"z) C_ ran F /\ (F"z) =/= (/))))
11		raleq 2266	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F"z) -> (A.f e. w -. fSu <-> A.f e. (F"z) -. fSu))
12	11	rexeqbi1dv 2272	. . . . . . . . . . . . . . . . . . . . . . . 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 688	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w = (F"z) -> (((w C_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu) <-> (((F"z) C_ ran F /\ (F"z) =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
14	13	cla4gv 2364	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F"z) e. _V -> (A.w((w C_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu) -> (((F"z) C_ ran F /\ (F"z) =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
15		funfvima2 4829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Fun F /\ z C_ dom F) -> (w e. z -> (F` w) e. (F"z)))
16		ne0i 2881	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F` w) e. (F"z) -> (F"z) =/= (/))
17	15, 16	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Fun F /\ z C_ dom F) -> (w e. z -> (F"z) =/= (/)))
18	17	19.23adv 1584	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun F /\ z C_ dom F) -> (E.w w e. z -> (F"z) =/= (/)))
19		n0 2884	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z =/= (/) <-> E.w w e. z)
20	18, 19	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((Fun F /\ z C_ dom F) -> (z =/= (/) -> (F"z) =/= (/)))
21	20	imp 377	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((Fun F /\ z C_ dom F) /\ z =/= (/)) -> (F"z) =/= (/))
22		imassrn 4278	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F"z) C_ ran F
23	21, 22	jctil 316	. . . . . . . . . . . . . . . . . . . . . 22 |- (((Fun F /\ z C_ dom F) /\ z =/= (/)) -> ((F"z) C_ ran F /\ (F"z) =/= (/)))
24	14, 23	syl7 26	. . . . . . . . . . . . . . . . . . . . 21 |- ((F"z) e. _V -> (A.w((w C_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu) -> (((Fun F /\ z C_ dom F) /\ z =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
25	7, 24	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (Fun F -> (A.w((w C_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu) -> (((Fun F /\ z C_ dom F) /\ z =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
26		df-fr 3625	. . . . . . . . . . . . . . . . . . . 20 |- (S Fr ran F <-> A.w((w C_ ran F /\ w =/= (/)) -> E.u e. w A.f e. w -. fSu))
27	25, 26	syl5ib 223	. . . . . . . . . . . . . . . . . . 19 |- (Fun F -> (S Fr ran F -> (((Fun F /\ z C_ dom F) /\ z =/= (/)) -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
28	27	com23 36	. . . . . . . . . . . . . . . . . 18 |- (Fun F -> (((Fun F /\ z C_ dom F) /\ z =/= (/)) -> (S Fr ran F -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
29	28	exp3a 405	. . . . . . . . . . . . . . . . 17 |- (Fun F -> ((Fun F /\ z C_ dom F) -> (z =/= (/) -> (S Fr ran F -> E.u e. (F"z)A.f e. (F"z) -. fSu))))
30	29	anabsi5 553	. . . . . . . . . . . . . . . 16 |- ((Fun F /\ z C_ dom F) -> (z =/= (/) -> (S Fr ran F -> E.u e. (F"z)A.f e. (F"z) -. fSu)))
31	30	imp3a 388	. . . . . . . . . . . . . . 15 |- ((Fun F /\ z C_ dom F) -> ((z =/= (/) /\ S Fr ran F) -> E.u e. (F"z)A.f e. (F"z) -. fSu))
32		fores 4627	. . . . . . . . . . . . . . . 16 |- ((Fun F /\ z C_ dom F) -> (F |` z):z-onto->(F"z))
33		breq1 3341	. . . . . . . . . . . . . . . . . . . . 21 |- (((F |` z)` v) = f -> (((F |` z)` v)S((F |` z)` w) <-> fS((F |` z)` w)))
34	33	notbid 673	. . . . . . . . . . . . . . . . . . . 20 |- (((F |` z)` v) = f -> (-. ((F |` z)` v)S((F |` z)` w) <-> -. fS((F |` z)` w)))
35	34	cbvfo 4861	. . . . . . . . . . . . . . . . . . 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 2124	. . . . . . . . . . . . . . . . . 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 3342	. . . . . . . . . . . . . . . . . . . . 21 |- (((F |` z)` w) = u -> (fS((F |` z)` w) <-> fSu))
38	37	notbid 673	. . . . . . . . . . . . . . . . . . . 20 |- (((F |` z)` w) = u -> (-. fS((F |` z)` w) <-> -. fSu))
39	38	ralbidv 2123	. . . . . . . . . . . . . . . . . . 19 |- (((F |` z)` w) = u -> (A.f e. (F"z) -. fS((F |` z)` w) <-> A.f e. (F"z) -. fSu))
40	39	cbvexfo 4862	. . . . . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . . . . 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 4691	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. z -> ((F |` z)` v) = (F` v))
43		fvres 4691	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. z -> ((F |` z)` w) = (F` w))
44	42, 43	breqan12rd 3355	. . . . . . . . . . . . . . . . . . . . 21 |- ((w e. z /\ v e. z) -> (((F |` z)` v)S((F |` z)` w) <-> (F` v)S(F` w)))
45		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- v e. _V
46		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22 |- w e. _V
47		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = v -> (F` x) = (F` v))
48	47	breq1d 3348	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = v -> ((F` x)S(F` y) <-> (F` v)S(F` y)))
49		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = w -> (F` y) = (F` w))
50	49	breq2d 3350	. . . . . . . . . . . . . . . . . . . . . 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 3571	. . . . . . . . . . . . . . . . . . . . 21 |- (vRw <-> (F` v)S(F` w))
53	44, 52	syl6rbbr 598	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. z /\ v e. z) -> (vRw <-> ((F |` z)` v)S((F |` z)` w)))
54	53	notbid 673	. . . . . . . . . . . . . . . . . . 19 |- ((w e. z /\ v e. z) -> (-. vRw <-> -. ((F |` z)` v)S((F |` z)` w)))
55	54	ralbidva 2119	. . . . . . . . . . . . . . . . . 18 |- (w e. z -> (A.v e. z -. vRw <-> A.v e. z -. ((F |` z)` v)S((F |` z)` w)))
56	55	rexbiia 2134	. . . . . . . . . . . . . . . . 17 |- (E.w e. z A.v e. z -. vRw <-> E.w e. z A.v e. z -. ((F |` z)` v)S((F |` z)` w))
57	41, 56	syl5bb 591	. . . . . . . . . . . . . . . 16 |- ((F |` z):z-onto->(F"z) -> (E.w e. z A.v e. z -. vRw <-> E.u e. (F"z)A.f e. (F"z) -. fSu))
58	32, 57	syl 12	. . . . . . . . . . . . . . 15 |- ((Fun F /\ z C_ dom F) -> (E.w e. z A.v e. z -. vRw <-> E.u e. (F"z)A.f e. (F"z) -. fSu))
59	31, 58	sylibrd 221	. . . . . . . . . . . . . 14 |- ((Fun F /\ z C_ dom F) -> ((z =/= (/) /\ S Fr ran F) -> E.w e. z A.v e. z -. vRw))
60	59	exp4b 410	. . . . . . . . . . . . 13 |- (Fun F -> (z C_ dom F -> (z =/= (/) -> (S Fr ran F -> E.w e. z A.v e. z -. vRw))))
61	60	com34 40	. . . . . . . . . . . 12 |- (Fun F -> (z C_ dom F -> (S Fr ran F -> (z =/= (/) -> E.w e. z A.v e. z -. vRw))))
62	61	com23 36	. . . . . . . . . . 11 |- (Fun F -> (S Fr ran F -> (z C_ dom F -> (z =/= (/) -> E.w e. z A.v e. z -. vRw))))
63	62	imp4a 391	. . . . . . . . . 10 |- (Fun F -> (S Fr ran F -> ((z C_ dom F /\ z =/= (/)) -> E.w e. z A.v e. z -. vRw)))
64	63	19.21adv 1666	. . . . . . . . 9 |- (Fun F -> (S Fr ran F -> A.z((z C_ dom F /\ z =/= (/)) -> E.w e. z A.v e. z -. vRw)))
65		df-fr 3625	. . . . . . . . 9 |- (R Fr dom F <-> A.z((z C_ dom F /\ z =/= (/)) -> E.w e. z A.v e. z -. vRw))
66	64, 65	syl6ibr 230	. . . . . . . 8 |- (Fun F -> (S Fr ran F -> R Fr dom F))
67		freq2 3633	. . . . . . . . 9 |- (dom F = A -> (R Fr dom F <-> R Fr A))
68	67	biimpd 170	. . . . . . . 8 |- (dom F = A -> (R Fr dom F -> R Fr A))
69	66, 68	sylan9 517	. . . . . . 7 |- ((Fun F /\ dom F = A) -> (S Fr ran F -> R Fr A))
70	5, 69	sylbi 216	. . . . . 6 |- (F Fn A -> (S Fr ran F -> R Fr A))
71	4, 70	sylan9r 519	. . . . 5 |- ((F Fn A /\ ran F = B) -> (S Fr B -> R Fr A))
72	2, 71	sylbi 216	. . . 4 |- (F:A-onto->B -> (S Fr B -> R Fr A))
73	1, 72	syl 12	. . 3 |- (F:A-1-1-onto->B -> (S Fr B -> R Fr A))
74		df-f1o 4013	. . . . 5 |- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
75		fveq2 4681	. . . . . . . . . . 11 |- (x = w -> (F` x) = (F` w))
76	75	breq1d 3348	. . . . . . . . . 10 |- (x = w -> ((F` x)S(F` y) <-> (F` w)S(F` y)))
77		fveq2 4681	. . . . . . . . . . 11 |- (y = v -> (F` y) = (F` v))
78	77	breq2d 3350	. . . . . . . . . 10 |- (y = v -> ((F` w)S(F` y) <-> (F` w)S(F` v)))
79	46, 45, 76, 78, 51	brab 3571	. . . . . . . . 9 |- (wRv <-> (F` w)S(F` v))
80	79	a1i 8	. . . . . . . 8 |- ((F:A-1-1->B /\ (w e. A /\ v e. A)) -> (wRv <-> (F` w)S(F` v)))
81		f1fveq 4852	. . . . . . . . 9 |- ((F:A-1-1->B /\ (w e. A /\ v e. A)) -> ((F` w) = (F` v) <-> w = v))
82	81	bicomd 580	. . . . . . . 8 |- ((F:A-1-1->B /\ (w e. A /\ v e. A)) -> (w = v <-> (F` w) = (F` v)))
83	52	a1i 8	. . . . . . . 8 |- ((F:A-1-1->B /\ (w e. A /\ v e. A)) -> (vRw <-> (F` v)S(F` w)))
84	80, 82, 83	3orbi123d 1167	. . . . . . 7 |- ((F:A-1-1->B /\ (w e. A /\ v e. A)) -> ((wRv \/ w = v \/ vRw) <-> ((F` w)S(F` v) \/ (F` w) = (F` v) \/ (F` v)S(F` w))))
85	84	2ralbidva 2138	. . . . . 6 |- (F:A-1-1->B -> (A.w e. A A.v e. A (wRv \/ w = v \/ vRw) <-> A.w e. A A.v e. A ((F` w)S(F` v) \/ (F` w) = (F` v) \/ (F` v)S(F` w))))
86		breq1 3341	. . . . . . . . . 10 |- ((F` w) = u -> ((F` w)S(F` v) <-> uS(F` v)))
87		eqeq1 1890	. . . . . . . . . 10 |- ((F` w) = u -> ((F` w) = (F` v) <-> u = (F` v)))
88		breq2 3342	. . . . . . . . . 10 |- ((F` w) = u -> ((F` v)S(F` w) <-> (F` v)Su))
89	86, 87, 88	3orbi123d 1167	. . . . . . . . 9 |- ((F` w) = u -> (((F` w)S(F` v) \/ (F` w) = (F` v) \/ (F` v)S(F` w)) <-> (uS(F` v) \/ u = (F` v) \/ (F` v)Su)))
90	89	ralbidv 2123	. . . . . . . 8 |- ((F` w) = u -> (A.v e. A ((F` w)S(F` v) \/ (F` w) = (F` v) \/ (F` v)S(F` w)) <-> A.v e. A (uS(F` v) \/ u = (F` v) \/ (F` v)Su)))
91	90	cbvfo 4861	. . . . . . 7 |- (F:A-onto->B -> (A.w e. A A.v e. A ((F` w)S(F` v) \/ (F` w) = (F` v) \/ (F` v)S(F` w)) <-> A.u e. B A.v e. A (uS(F` v) \/ u = (F` v) \/ (F` v)Su)))
92		breq2 3342	. . . . . . . . . 10 |- ((F` v) = f -> (uS(F` v) <-> uSf))
93		eqeq2 1893	. . . . . . . . . 10 |- ((F` v) = f -> (u = (F` v) <-> u = f))
94		breq1 3341	. . . . . . . . . 10 |- ((F` v) = f -> ((F` v)Su <-> fSu))
95	92, 93, 94	3orbi123d 1167	. . . . . . . . 9 |- ((F` v) = f -> ((uS(F` v) \/ u = (F` v) \/ (F` v)Su) <-> (uSf \/ u = f \/ fSu)))
96	95	cbvfo 4861	. . . . . . . 8 |- (F:A-onto->B -> (A.v e. A (uS(F` v) \/ u = (F` v) \/ (F` v)Su) <-> A.f e. B (uSf \/ u = f \/ fSu)))
97	96	ralbidv 2123	. . . . . . 7 |- (F:A-onto->B -> (A.u e. B A.v e. A (uS(F` v) \/ u = (F` v) \/ (F` v)Su) <-> A.u e. B A.f e. B (uSf \/ u = f \/ fSu)))
98	91, 97	bitrd 587	. . . . . 6 |- (F:A-onto->B -> (A.w e. A A.v e. A ((F` w)S(F` v) \/ (F` w) = (F` v) \/ (F` v)S(F` w)) <-> A.u e. B A.f e. B (uSf \/ u = f \/ fSu)))
99	85, 98	sylan9bb 599	. . . . 5 |- ((F:A-1-1->B /\ F:A-onto->B) -> (A.w e. A A.v e. A (wRv \/ w = v \/ vRw) <-> A.u e. B A.f e. B (uSf \/ u = f \/ fSu)))
100	74, 99	sylbi 216	. . . 4 |- (F:A-1-1-onto->B -> (A.w e. A A.v e. A (wRv \/ w = v \/ vRw) <-> A.u e. B A.f e. B (uSf \/ u = f \/ fSu)))
101	100	biimprd 171	. . 3 |- (F:A-1-1-onto->B -> (A.u e. B A.f e. B (uSf \/ u = f \/ fSu) -> A.w e. A A.v e. A (wRv \/ w = v \/ vRw)))
102	73, 101	anim12d 617	. 2 |- (F:A-1-1-onto->B -> ((S Fr B /\ A.u e. B A.f e. B (uSf \/ u = f \/ fSu)) -> (R Fr A /\ A.w e. A A.v e. A (wRv \/ w = v \/ vRw))))
103		dfwe2 3861	. 2 |- (S We B <-> (S Fr B /\ A.u e. B A.f e. B (uSf \/ u = f \/ fSu)))
104		dfwe2 3861	. 2 |- (R We A <-> (R Fr A /\ A.w e. A A.v e. A (wRv \/ w = v \/ vRw)))
105	102, 103, 104	3imtr4g 612	1 |- (F:A-1-1-onto->B -> (S We B -> R We A))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   C_ wss 2593  (/)c0 2875   class class class wbr 3338  {copab 3395   Fr wfr 3623   We wwe 3624  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014

Copyright terms: Public domain