Theorem ordiso 5683

Description: Order-isomorphic ordinal numbers are equal. (Contributed by Jeff Hankins, 16-Oct-2009.)

Assertion

Ref	Expression
ordiso	|- ((A e. On /\ B e. On) -> (A = B <-> E.f f Isom _E , _E (A, B)))

Distinct variable groups:   A,f   B,f

Proof of Theorem ordiso

Step	Hyp	Ref	Expression
1		resiexg 4253	. . . . 5 |- (A e. On -> ( _I |` A) e. _V)
2	1	3ad2ant1 897	. . . 4 |- ((A e. On /\ B e. On /\ A = B) -> ( _I |` A) e. _V)
3		df-iso 4015	. . . . 5 |- (( _I |` A) Isom _E , _E (A, B) <-> (( _I |` A):A-1-1-onto->B /\ A.x e. A A.y e. A (x _E y <-> (( _I |` A)` x) _E (( _I |` A)` y))))
4		f1oi 4671	. . . . . 6 |- ( _I |` A):A-1-1-onto->A
5		f1oeq3 4632	. . . . . . 7 |- (A = B -> (( _I |` A):A-1-1-onto->A <-> ( _I |` A):A-1-1-onto->B))
6	5	3ad2ant3 899	. . . . . 6 |- ((A e. On /\ B e. On /\ A = B) -> (( _I |` A):A-1-1-onto->A <-> ( _I |` A):A-1-1-onto->B))
7	4, 6	mpbii 210	. . . . 5 |- ((A e. On /\ B e. On /\ A = B) -> ( _I |` A):A-1-1-onto->B)
8		fvresi 4819	. . . . . . . . . 10 |- (x e. A -> (( _I |` A)` x) = x)
9	8	ad2antrl 442	. . . . . . . . 9 |- (((A e. On /\ B e. On /\ A = B) /\ (x e. A /\ y e. A)) -> (( _I |` A)` x) = x)
10		fvresi 4819	. . . . . . . . . 10 |- (y e. A -> (( _I |` A)` y) = y)
11	10	ad2antll 443	. . . . . . . . 9 |- (((A e. On /\ B e. On /\ A = B) /\ (x e. A /\ y e. A)) -> (( _I |` A)` y) = y)
12	9, 11	breq12d 3351	. . . . . . . 8 |- (((A e. On /\ B e. On /\ A = B) /\ (x e. A /\ y e. A)) -> ((( _I |` A)` x) _E (( _I |` A)` y) <-> x _E y))
13	12	bicomd 580	. . . . . . 7 |- (((A e. On /\ B e. On /\ A = B) /\ (x e. A /\ y e. A)) -> (x _E y <-> (( _I |` A)` x) _E (( _I |` A)` y)))
14	13	ex 402	. . . . . 6 |- ((A e. On /\ B e. On /\ A = B) -> ((x e. A /\ y e. A) -> (x _E y <-> (( _I |` A)` x) _E (( _I |` A)` y))))
15	14	r19.21aivv 2183	. . . . 5 |- ((A e. On /\ B e. On /\ A = B) -> A.x e. A A.y e. A (x _E y <-> (( _I |` A)` x) _E (( _I |` A)` y)))
16	3, 7, 15	sylanbrc 527	. . . 4 |- ((A e. On /\ B e. On /\ A = B) -> ( _I |` A) Isom _E , _E (A, B))
17		isoeq1 4863	. . . . 5 |- (f = ( _I |` A) -> (f Isom _E , _E (A, B) <-> ( _I |` A) Isom _E , _E (A, B)))
18	17	cla4egv 2365	. . . 4 |- (( _I |` A) e. _V -> (( _I |` A) Isom _E , _E (A, B) -> E.f f Isom _E , _E (A, B)))
19	2, 16, 18	sylc 83	. . 3 |- ((A e. On /\ B e. On /\ A = B) -> E.f f Isom _E , _E (A, B))
20	19	3expia 1069	. 2 |- ((A e. On /\ B e. On) -> (A = B -> E.f f Isom _E , _E (A, B)))
21		simpllr 453	. . . . . . . . . . . . . . . . 17 |- ((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) -> B e. On)
22	21	ad2antrr 440	. . . . . . . . . . . . . . . 16 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> B e. On)
23		simpr 350	. . . . . . . . . . . . . . . . 17 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> z e. (f` x))
24		isof1o 4870	. . . . . . . . . . . . . . . . . . . . 21 |- (f Isom _E , _E (A, B) -> f:A-1-1-onto->B)
25		f1of 4635	. . . . . . . . . . . . . . . . . . . . 21 |- (f:A-1-1-onto->B -> f:A-->B)
26	24, 25	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (f Isom _E , _E (A, B) -> f:A-->B)
27	26	ad2antlr 441	. . . . . . . . . . . . . . . . . . 19 |- ((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) -> f:A-->B)
28	27	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> f:A-->B)
29		simplrr 455	. . . . . . . . . . . . . . . . . 18 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> x e. A)
30		ffvelrn 4787	. . . . . . . . . . . . . . . . . 18 |- ((f:A-->B /\ x e. A) -> (f` x) e. B)
31	28, 29, 30	syl11anc 524	. . . . . . . . . . . . . . . . 17 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> (f` x) e. B)
32	23, 31	jca 310	. . . . . . . . . . . . . . . 16 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> (z e. (f` x) /\ (f` x) e. B))
33		ontr1 3710	. . . . . . . . . . . . . . . 16 |- (B e. On -> ((z e. (f` x) /\ (f` x) e. B) -> z e. B))
34	22, 32, 33	sylc 83	. . . . . . . . . . . . . . 15 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> z e. B)
35		f1ofo 4643	. . . . . . . . . . . . . . . . . 18 |- (f:A-1-1-onto->B -> f:A-onto->B)
36		forn 4620	. . . . . . . . . . . . . . . . . 18 |- (f:A-onto->B -> ran f = B)
37	24, 35, 36	3syl 24	. . . . . . . . . . . . . . . . 17 |- (f Isom _E , _E (A, B) -> ran f = B)
38	37	ad2antlr 441	. . . . . . . . . . . . . . . 16 |- ((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) -> ran f = B)
39	38	ad2antrr 440	. . . . . . . . . . . . . . 15 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> ran f = B)
40	34, 39	eleqtrrd 1974	. . . . . . . . . . . . . 14 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> z e. ran f)
41		f1ofn 4636	. . . . . . . . . . . . . . . . 17 |- (f:A-1-1-onto->B -> f Fn A)
42		fvelrnb 4719	. . . . . . . . . . . . . . . . 17 |- (f Fn A -> (z e. ran f <-> E.w e. A (f` w) = z))
43	24, 41, 42	3syl 24	. . . . . . . . . . . . . . . 16 |- (f Isom _E , _E (A, B) -> (z e. ran f <-> E.w e. A (f` w) = z))
44	43	ad2antlr 441	. . . . . . . . . . . . . . 15 |- ((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) -> (z e. ran f <-> E.w e. A (f` w) = z))
45	44	ad2antrr 440	. . . . . . . . . . . . . 14 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> (z e. ran f <-> E.w e. A (f` w) = z))
46	40, 45	mpbid 212	. . . . . . . . . . . . 13 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> E.w e. A (f` w) = z)
47		simprrr 459	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> (f` w) = z)
48		simprl 450	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> z e. (f` x))
49	47, 48	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . 20 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> (f` w) e. (f` x))
50		fvex 4689	. . . . . . . . . . . . . . . . . . . . 21 |- (f` w) e. _V
51		fvex 4689	. . . . . . . . . . . . . . . . . . . . 21 |- (f` x) e. _V
52	50, 51	epelc 3584	. . . . . . . . . . . . . . . . . . . 20 |- ((f` w) _E (f` x) <-> (f` w) e. (f` x))
53	49, 52	sylibr 217	. . . . . . . . . . . . . . . . . . 19 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> (f` w) _E (f` x))
54		simplr 449	. . . . . . . . . . . . . . . . . . . . 21 |- ((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) -> f Isom _E , _E (A, B))
55	54	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> f Isom _E , _E (A, B))
56		simprrl 458	. . . . . . . . . . . . . . . . . . . 20 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> w e. A)
57		simplrr 455	. . . . . . . . . . . . . . . . . . . 20 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> x e. A)
58		isorel 4871	. . . . . . . . . . . . . . . . . . . 20 |- ((f Isom _E , _E (A, B) /\ (w e. A /\ x e. A)) -> (w _E x <-> (f` w) _E (f` x)))
59	55, 56, 57, 58	syl12anc 1098	. . . . . . . . . . . . . . . . . . 19 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> (w _E x <-> (f` w) _E (f` x)))
60	53, 59	mpbird 213	. . . . . . . . . . . . . . . . . 18 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> w _E x)
61		epel 3585	. . . . . . . . . . . . . . . . . 18 |- (w _E x <-> w e. x)
62	60, 61	sylib 215	. . . . . . . . . . . . . . . . 17 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> w e. x)
63		simprr 451	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. (f` x) /\ (w e. A /\ (f` w) = z)) -> (f` w) = z)
64	63	ad2antrl 442	. . . . . . . . . . . . . . . . . . . 20 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ ((z e. (f` x) /\ (w e. A /\ (f` w) = z)) /\ w e. x)) -> (f` w) = z)
65		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = w -> (y e. A <-> w e. A))
66		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = w -> (f` y) = (f` w))
67		id 73	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = w -> y = w)
68	66, 67	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = w -> ((f` y) = y <-> (f` w) = w))
69	65, 68	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = w -> ((y e. A -> (f` y) = y) <-> (w e. A -> (f` w) = w)))
70	69	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w e. x -> (A.y e. x (y e. A -> (f` y) = y) -> (w e. A -> (f` w) = w)))
71		ontr1 3710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (A e. On -> ((w e. x /\ x e. A) -> w e. A))
72	71	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (A e. On -> (w e. x -> (x e. A -> w e. A)))
73	72	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. x -> (A e. On -> (x e. A -> w e. A)))
74		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. A -> ((w e. A -> (f` w) = w) -> (f` w) = w))
75	73, 74	syl8 27	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. x -> (A e. On -> (x e. A -> ((w e. A -> (f` w) = w) -> (f` w) = w))))
76	75	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w e. x -> ((w e. A -> (f` w) = w) -> (x e. A -> (A e. On -> (f` w) = w))))
77	70, 76	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w e. x -> (A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (A e. On -> (f` w) = w))))
78	77	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A e. On -> (A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (w e. x -> (f` w) = w))))
79	78	imp42 396	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A e. On /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ w e. x) -> (f` w) = w)
80	79	adantllr 433	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((A e. On /\ B e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ w e. x) -> (f` w) = w)
81	80	adantllr 433	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ w e. x) -> (f` w) = w)
82	81	adantllr 433	. . . . . . . . . . . . . . . . . . . . 21 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ w e. x) -> (f` w) = w)
83	82	adantrl 430	. . . . . . . . . . . . . . . . . . . 20 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ ((z e. (f` x) /\ (w e. A /\ (f` w) = z)) /\ w e. x)) -> (f` w) = w)
84	64, 83	eqtr3d 1927	. . . . . . . . . . . . . . . . . . 19 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ ((z e. (f` x) /\ (w e. A /\ (f` w) = z)) /\ w e. x)) -> z = w)
85		simprr 451	. . . . . . . . . . . . . . . . . . 19 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ ((z e. (f` x) /\ (w e. A /\ (f` w) = z)) /\ w e. x)) -> w e. x)
86	84, 85	eqeltrd 1971	. . . . . . . . . . . . . . . . . 18 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ ((z e. (f` x) /\ (w e. A /\ (f` w) = z)) /\ w e. x)) -> z e. x)
87	86	expr 418	. . . . . . . . . . . . . . . . 17 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> (w e. x -> z e. x))
88	62, 87	mpd 29	. . . . . . . . . . . . . . . 16 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ (z e. (f` x) /\ (w e. A /\ (f` w) = z))) -> z e. x)
89	88	expr 418	. . . . . . . . . . . . . . 15 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> ((w e. A /\ (f` w) = z) -> z e. x))
90	89	exp3a 405	. . . . . . . . . . . . . 14 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> (w e. A -> ((f` w) = z -> z e. x)))
91	90	r19.23adv 2215	. . . . . . . . . . . . 13 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> (E.w e. A (f` w) = z -> z e. x))
92	46, 91	mpd 29	. . . . . . . . . . . 12 |- ((((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) /\ z e. (f` x)) -> z e. x)
93	92	ex 402	. . . . . . . . . . 11 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) -> (z e. (f` x) -> z e. x))
94		eleq1 1957	. . . . . . . . . . . . . . . . . . . . 21 |- (y = z -> (y e. A <-> z e. A))
95		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = z -> (f` y) = (f` z))
96		id 73	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = z -> y = z)
97	95, 96	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . 21 |- (y = z -> ((f` y) = y <-> (f` z) = z))
98	94, 97	imbi12d 688	. . . . . . . . . . . . . . . . . . . 20 |- (y = z -> ((y e. A -> (f` y) = y) <-> (z e. A -> (f` z) = z)))
99	98	rcla4v 2376	. . . . . . . . . . . . . . . . . . 19 |- (z e. x -> (A.y e. x (y e. A -> (f` y) = y) -> (z e. A -> (f` z) = z)))
100		ontr1 3710	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. On -> ((z e. x /\ x e. A) -> z e. A))
101	100	exp3a 405	. . . . . . . . . . . . . . . . . . . . . 22 |- (A e. On -> (z e. x -> (x e. A -> z e. A)))
102	101	com12 14	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. x -> (A e. On -> (x e. A -> z e. A)))
103		pm2.27 76	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. A -> ((z e. A -> (f` z) = z) -> (f` z) = z))
104	102, 103	syl8 27	. . . . . . . . . . . . . . . . . . . 20 |- (z e. x -> (A e. On -> (x e. A -> ((z e. A -> (f` z) = z) -> (f` z) = z))))
105	104	com24 41	. . . . . . . . . . . . . . . . . . 19 |- (z e. x -> ((z e. A -> (f` z) = z) -> (x e. A -> (A e. On -> (f` z) = z))))
106	99, 105	syld 30	. . . . . . . . . . . . . . . . . 18 |- (z e. x -> (A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (A e. On -> (f` z) = z))))
107	106	com14 42	. . . . . . . . . . . . . . . . 17 |- (A e. On -> (A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (z e. x -> (f` z) = z))))
108	107	imp44 398	. . . . . . . . . . . . . . . 16 |- ((A e. On /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> (f` z) = z)
109	108	adantlr 429	. . . . . . . . . . . . . . 15 |- (((A e. On /\ B e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> (f` z) = z)
110	109	adantlr 429	. . . . . . . . . . . . . 14 |- ((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> (f` z) = z)
111	110	adantlr 429	. . . . . . . . . . . . 13 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> (f` z) = z)
112		epel 3585	. . . . . . . . . . . . . . . . 17 |- (z _E x <-> z e. x)
113	112	biimpri 169	. . . . . . . . . . . . . . . 16 |- (z e. x -> z _E x)
114	113	ad2antll 443	. . . . . . . . . . . . . . 15 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> z _E x)
115		simpllr 453	. . . . . . . . . . . . . . . 16 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> f Isom _E , _E (A, B))
116	100	ancomsd 485	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. On -> ((x e. A /\ z e. x) -> z e. A))
117	116	imp 377	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. On /\ (x e. A /\ z e. x)) -> z e. A)
118	117	adantlr 429	. . . . . . . . . . . . . . . . . . 19 |- (((A e. On /\ B e. On) /\ (x e. A /\ z e. x)) -> z e. A)
119	118	adantlr 429	. . . . . . . . . . . . . . . . . 18 |- ((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ (x e. A /\ z e. x)) -> z e. A)
120	119	adantlr 429	. . . . . . . . . . . . . . . . 17 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (x e. A /\ z e. x)) -> z e. A)
121	120	adantrll 436	. . . . . . . . . . . . . . . 16 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> z e. A)
122		simprlr 457	. . . . . . . . . . . . . . . 16 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> x e. A)
123		isorel 4871	. . . . . . . . . . . . . . . 16 |- ((f Isom _E , _E (A, B) /\ (z e. A /\ x e. A)) -> (z _E x <-> (f` z) _E (f` x)))
124	115, 121, 122, 123	syl12anc 1098	. . . . . . . . . . . . . . 15 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> (z _E x <-> (f` z) _E (f` x)))
125	114, 124	mpbid 212	. . . . . . . . . . . . . 14 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> (f` z) _E (f` x))
126		fvex 4689	. . . . . . . . . . . . . . 15 |- (f` z) e. _V
127	126, 51	epelc 3584	. . . . . . . . . . . . . 14 |- ((f` z) _E (f` x) <-> (f` z) e. (f` x))
128	125, 127	sylib 215	. . . . . . . . . . . . 13 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> (f` z) e. (f` x))
129	111, 128	eqeltrrd 1972	. . . . . . . . . . . 12 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ ((A.y e. x (y e. A -> (f` y) = y) /\ x e. A) /\ z e. x)) -> z e. (f` x))
130	129	expr 418	. . . . . . . . . . 11 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) -> (z e. x -> z e. (f` x)))
131	93, 130	impbid 574	. . . . . . . . . 10 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) -> (z e. (f` x) <-> z e. x))
132	131	eqrdv 1882	. . . . . . . . 9 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ x e. On) /\ (A.y e. x (y e. A -> (f` y) = y) /\ x e. A)) -> (f` x) = x)
133	132	exp43 415	. . . . . . . 8 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (x e. On -> (A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (f` x) = x))))
134	133	r19.21aiv 2175	. . . . . . 7 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> A.x e. On (A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (f` x) = x)))
135		iman 256	. . . . . . . . . . . 12 |- ((y e. A -> (f` y) = y) <-> -. (y e. A /\ -. (f` y) = y))
136	135	ralbii 2127	. . . . . . . . . . 11 |- (A.y e. x (y e. A -> (f` y) = y) <-> A.y e. x -. (y e. A /\ -. (f` y) = y))
137		iman 256	. . . . . . . . . . 11 |- ((x e. A -> (f` x) = x) <-> -. (x e. A /\ -. (f` x) = x))
138	136, 137	imbi12i 205	. . . . . . . . . 10 |- ((A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (f` x) = x)) <-> (A.y e. x -. (y e. A /\ -. (f` y) = y) -> -. (x e. A /\ -. (f` x) = x)))
139		imnan 261	. . . . . . . . . 10 |- ((A.y e. x -. (y e. A /\ -. (f` y) = y) -> -. (x e. A /\ -. (f` x) = x)) <-> -. (A.y e. x -. (y e. A /\ -. (f` y) = y) /\ (x e. A /\ -. (f` x) = x)))
140		ancom 482	. . . . . . . . . . 11 |- ((A.y e. x -. (y e. A /\ -. (f` y) = y) /\ (x e. A /\ -. (f` x) = x)) <-> ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)))
141	140	notbii 204	. . . . . . . . . 10 |- (-. (A.y e. x -. (y e. A /\ -. (f` y) = y) /\ (x e. A /\ -. (f` x) = x)) <-> -. ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)))
142	138, 139, 141	3bitri 194	. . . . . . . . 9 |- ((A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (f` x) = x)) <-> -. ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)))
143	142	ralbii 2127	. . . . . . . 8 |- (A.x e. On (A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (f` x) = x)) <-> A.x e. On -. ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)))
144		ralnex 2113	. . . . . . . 8 |- (A.x e. On -. ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)) <-> -. E.x e. On ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)))
145	143, 144	bitri 190	. . . . . . 7 |- (A.x e. On (A.y e. x (y e. A -> (f` y) = y) -> (x e. A -> (f` x) = x)) <-> -. E.x e. On ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)))
146	134, 145	sylib 215	. . . . . 6 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> -. E.x e. On ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)))
147		onelon 3683	. . . . . . . . . . . . 13 |- ((A e. On /\ x e. A) -> x e. On)
148	147	ex 402	. . . . . . . . . . . 12 |- (A e. On -> (x e. A -> x e. On))
149	148	adantrd 427	. . . . . . . . . . 11 |- (A e. On -> ((x e. A /\ -. (f` x) = x) -> x e. On))
150	149	ad2antrr 440	. . . . . . . . . 10 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> ((x e. A /\ -. (f` x) = x) -> x e. On))
151	150	ancrd 323	. . . . . . . . 9 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> ((x e. A /\ -. (f` x) = x) -> (x e. On /\ (x e. A /\ -. (f` x) = x))))
152	151	reximdv2 2200	. . . . . . . 8 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (E.x e. A -. (f` x) = x -> E.x e. On (x e. A /\ -. (f` x) = x)))
153		eleq1 1957	. . . . . . . . . 10 |- (x = y -> (x e. A <-> y e. A))
154		fveq2 4681	. . . . . . . . . . . 12 |- (x = y -> (f` x) = (f` y))
155		id 73	. . . . . . . . . . . 12 |- (x = y -> x = y)
156	154, 155	eqeq12d 1899	. . . . . . . . . . 11 |- (x = y -> ((f` x) = x <-> (f` y) = y))
157	156	notbid 673	. . . . . . . . . 10 |- (x = y -> (-. (f` x) = x <-> -. (f` y) = y))
158	153, 157	anbi12d 690	. . . . . . . . 9 |- (x = y -> ((x e. A /\ -. (f` x) = x) <-> (y e. A /\ -. (f` y) = y)))
159	158	onminex 3888	. . . . . . . 8 |- (E.x e. On (x e. A /\ -. (f` x) = x) -> E.x e. On ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y)))
160	152, 159	syl6 25	. . . . . . 7 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (E.x e. A -. (f` x) = x -> E.x e. On ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y))))
161		rexnal 2114	. . . . . . 7 |- (E.x e. A -. (f` x) = x <-> -. A.x e. A (f` x) = x)
162	160, 161	syl5ibr 224	. . . . . 6 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (-. A.x e. A (f` x) = x -> E.x e. On ((x e. A /\ -. (f` x) = x) /\ A.y e. x -. (y e. A /\ -. (f` y) = y))))
163	146, 162	mt3d 129	. . . . 5 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> A.x e. A (f` x) = x)
164		fveq2 4681	. . . . . . . . . . . . . 14 |- (x = z -> (f` x) = (f` z))
165		id 73	. . . . . . . . . . . . . 14 |- (x = z -> x = z)
166	164, 165	eqeq12d 1899	. . . . . . . . . . . . 13 |- (x = z -> ((f` x) = x <-> (f` z) = z))
167	166	rcla4cva 2379	. . . . . . . . . . . 12 |- ((A.x e. A (f` x) = x /\ z e. A) -> (f` z) = z)
168	167	adantll 428	. . . . . . . . . . 11 |- (((f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x) /\ z e. A) -> (f` z) = z)
169	168	adantll 428	. . . . . . . . . 10 |- ((((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) /\ z e. A) -> (f` z) = z)
170		ffvelrn 4787	. . . . . . . . . . . . 13 |- ((f:A-->B /\ z e. A) -> (f` z) e. B)
171	170, 26	sylan 497	. . . . . . . . . . . 12 |- ((f Isom _E , _E (A, B) /\ z e. A) -> (f` z) e. B)
172	171	adantll 428	. . . . . . . . . . 11 |- ((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ z e. A) -> (f` z) e. B)
173	172	adantlrr 435	. . . . . . . . . 10 |- ((((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) /\ z e. A) -> (f` z) e. B)
174	169, 173	eqeltrrd 1972	. . . . . . . . 9 |- ((((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) /\ z e. A) -> z e. B)
175	174	ex 402	. . . . . . . 8 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> (z e. A -> z e. B))
176	37	ad2antrl 442	. . . . . . . . . . 11 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> ran f = B)
177	176	eleq2d 1964	. . . . . . . . . 10 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> (z e. ran f <-> z e. B))
178	43	ad2antrl 442	. . . . . . . . . 10 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> (z e. ran f <-> E.w e. A (f` w) = z))
179	177, 178	bitr3d 589	. . . . . . . . 9 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> (z e. B <-> E.w e. A (f` w) = z))
180		fveq2 4681	. . . . . . . . . . . . . . . 16 |- (x = w -> (f` x) = (f` w))
181		id 73	. . . . . . . . . . . . . . . 16 |- (x = w -> x = w)
182	180, 181	eqeq12d 1899	. . . . . . . . . . . . . . 15 |- (x = w -> ((f` x) = x <-> (f` w) = w))
183	182	rcla4v 2376	. . . . . . . . . . . . . 14 |- (w e. A -> (A.x e. A (f` x) = x -> (f` w) = w))
184	183	a1i 8	. . . . . . . . . . . . 13 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (w e. A -> (A.x e. A (f` x) = x -> (f` w) = w)))
185		simpr 350	. . . . . . . . . . . . . . . . 17 |- (((f` w) = w /\ (f` w) = z) -> (f` w) = z)
186		simpl 346	. . . . . . . . . . . . . . . . 17 |- (((f` w) = w /\ (f` w) = z) -> (f` w) = w)
187	185, 186	eqtr3d 1927	. . . . . . . . . . . . . . . 16 |- (((f` w) = w /\ (f` w) = z) -> z = w)
188	187	adantl 424	. . . . . . . . . . . . . . 15 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ w e. A) /\ ((f` w) = w /\ (f` w) = z)) -> z = w)
189		simplr 449	. . . . . . . . . . . . . . 15 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ w e. A) /\ ((f` w) = w /\ (f` w) = z)) -> w e. A)
190	188, 189	eqeltrd 1971	. . . . . . . . . . . . . 14 |- (((((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) /\ w e. A) /\ ((f` w) = w /\ (f` w) = z)) -> z e. A)
191	190	exp43 415	. . . . . . . . . . . . 13 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (w e. A -> ((f` w) = w -> ((f` w) = z -> z e. A))))
192	184, 191	syldd 61	. . . . . . . . . . . 12 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (w e. A -> (A.x e. A (f` x) = x -> ((f` w) = z -> z e. A))))
193	192	com23 36	. . . . . . . . . . 11 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (A.x e. A (f` x) = x -> (w e. A -> ((f` w) = z -> z e. A))))
194	193	impr 422	. . . . . . . . . 10 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> (w e. A -> ((f` w) = z -> z e. A)))
195	194	r19.23adv 2215	. . . . . . . . 9 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> (E.w e. A (f` w) = z -> z e. A))
196	179, 195	sylbid 220	. . . . . . . 8 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> (z e. B -> z e. A))
197	175, 196	impbid 574	. . . . . . 7 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> (z e. A <-> z e. B))
198	197	eqrdv 1882	. . . . . 6 |- (((A e. On /\ B e. On) /\ (f Isom _E , _E (A, B) /\ A.x e. A (f` x) = x)) -> A = B)
199	198	expr 418	. . . . 5 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> (A.x e. A (f` x) = x -> A = B))
200	163, 199	mpd 29	. . . 4 |- (((A e. On /\ B e. On) /\ f Isom _E , _E (A, B)) -> A = B)
201	200	ex 402	. . 3 |- ((A e. On /\ B e. On) -> (f Isom _E , _E (A, B) -> A = B))
202	201	19.23adv 1584	. 2 |- ((A e. On /\ B e. On) -> (E.f f Isom _E , _E (A, B) -> A = B))
203	20, 202	impbid 574	1 |- ((A e. On /\ B e. On) -> (A = B <-> E.f f Isom _E , _E (A, B)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  E.wrex 2106  _Vcvv 2292   class class class wbr 3338   _E cep 3581   _I cid 3582  Oncon0 3657  ran crn 3987   |` cres 3988   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998   Isom wiso 3999

This theorem is referenced by:  ordtype 5691  ordtypeOLD 15382

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-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-pss 2607  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  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  df-iso 4015

Copyright terms: Public domain