Theorem hartog 5693

Description: Associate every set with an ordinal number known as its Hartog number. Apparently, this theorem has some sort of topological significance. I guess you would have to ask someone like Jeff Madsen or Dr. James Conant. Notice the similarity of this theorem to ondomon 6008, but unlike that theorem, this one does not require the Axiom of Choice ax-ac 5906. (Contributed by Jeff Hankins, 22-Oct-2009.)

Hypothesis

Ref	Expression
hartog.1	|- H = {x e. On | x ~<_ A}

Assertion

Ref	Expression
hartog	|- (A e. B -> H e. On)

Distinct variable group:   x,A

Proof of Theorem hartog

Step	Hyp	Ref	Expression
1		breq1 3341	. . . . . . . 8 |- (x = y -> (x ~<_ A <-> y ~<_ A))
2	1	elrab 2414	. . . . . . 7 |- (y e. {x e. On | x ~<_ A} <-> (y e. On /\ y ~<_ A))
3		onelon 3683	. . . . . . . . 9 |- ((z e. On /\ y e. z) -> y e. On)
4	3	ancoms 484	. . . . . . . 8 |- ((y e. z /\ z e. On) -> y e. On)
5	4	adantrr 431	. . . . . . 7 |- ((y e. z /\ (z e. On /\ z ~<_ A)) -> y e. On)
6		domtr 5474	. . . . . . . . 9 |- ((y ~<_ z /\ z ~<_ A) -> y ~<_ A)
7		onelss 3705	. . . . . . . . . . 11 |- (z e. On -> (y e. z -> y C_ z))
8	7	impcom 378	. . . . . . . . . 10 |- ((y e. z /\ z e. On) -> y C_ z)
9		visset 2295	. . . . . . . . . . 11 |- y e. _V
10		ssdomg 5467	. . . . . . . . . . 11 |- (y e. _V -> (y C_ z -> y ~<_ z))
11	9, 10	ax-mp 7	. . . . . . . . . 10 |- (y C_ z -> y ~<_ z)
12	8, 11	syl 12	. . . . . . . . 9 |- ((y e. z /\ z e. On) -> y ~<_ z)
13	6, 12	sylan 497	. . . . . . . 8 |- (((y e. z /\ z e. On) /\ z ~<_ A) -> y ~<_ A)
14	13	anasss 488	. . . . . . 7 |- ((y e. z /\ (z e. On /\ z ~<_ A)) -> y ~<_ A)
15	2, 5, 14	sylanbrc 527	. . . . . 6 |- ((y e. z /\ (z e. On /\ z ~<_ A)) -> y e. {x e. On | x ~<_ A})
16		breq1 3341	. . . . . . 7 |- (x = z -> (x ~<_ A <-> z ~<_ A))
17	16	elrab 2414	. . . . . 6 |- (z e. {x e. On | x ~<_ A} <-> (z e. On /\ z ~<_ A))
18	15, 17	sylan2b 501	. . . . 5 |- ((y e. z /\ z e. {x e. On | x ~<_ A}) -> y e. {x e. On | x ~<_ A})
19	18	gen2 1329	. . . 4 |- A.yA.z((y e. z /\ z e. {x e. On | x ~<_ A}) -> y e. {x e. On | x ~<_ A})
20		hartog.1	. . . . . 6 |- H = {x e. On | x ~<_ A}
21		treq 3417	. . . . . 6 |- (H = {x e. On | x ~<_ A} -> (Tr H <-> Tr {x e. On | x ~<_ A}))
22	20, 21	ax-mp 7	. . . . 5 |- (Tr H <-> Tr {x e. On | x ~<_ A})
23		dftr2 3413	. . . . 5 |- (Tr {x e. On | x ~<_ A} <-> A.yA.z((y e. z /\ z e. {x e. On | x ~<_ A}) -> y e. {x e. On | x ~<_ A}))
24	22, 23	bitri 190	. . . 4 |- (Tr H <-> A.yA.z((y e. z /\ z e. {x e. On | x ~<_ A}) -> y e. {x e. On | x ~<_ A}))
25	19, 24	mpbir 207	. . 3 |- Tr H
26		ssrab2 2692	. . . 4 |- {x e. On | x ~<_ A} C_ On
27	20, 26	eqsstri 2647	. . 3 |- H C_ On
28		ordon 3863	. . 3 |- Ord On
29		trssord 3675	. . 3 |- ((Tr H /\ H C_ On /\ Ord On) -> Ord H)
30	25, 27, 28, 29	mp3an 1191	. 2 |- Ord H
31		brdomg 5435	. . . . . . . . . 10 |- (A e. B -> (t ~<_ A <-> E.g g:t-1-1->A))
32		imassrn 4278	. . . . . . . . . . . . . . . . . . 19 |- (g"t) C_ ran g
33	32	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (g:t-1-1->A -> (g"t) C_ ran g)
34		f1f 4610	. . . . . . . . . . . . . . . . . . 19 |- (g:t-1-1->A -> g:t-->A)
35		frn 4569	. . . . . . . . . . . . . . . . . . 19 |- (g:t-->A -> ran g C_ A)
36	34, 35	syl 12	. . . . . . . . . . . . . . . . . 18 |- (g:t-1-1->A -> ran g C_ A)
37	33, 36	sstrd 2627	. . . . . . . . . . . . . . . . 17 |- (g:t-1-1->A -> (g"t) C_ A)
38	37	ad2antlr 441	. . . . . . . . . . . . . . . 16 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> (g"t) C_ A)
39		simprl 450	. . . . . . . . . . . . . . . . . . . . 21 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (m = <.a, b>. /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d))) -> m = <.a, b>.)
40		simprr1 924	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((c e. t /\ d e. t) /\ (a = (g` c) /\ b = (g` d) /\ c e. d))) -> a = (g` c))
41	34	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((A e. B /\ g:t-1-1->A) -> g:t-->A)
42	41	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (c e. t /\ d e. t)) -> g:t-->A)
43		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (c e. t /\ d e. t)) -> c e. t)
44		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((g:t-->A /\ c e. t) -> (g` c) e. A)
45	42, 43, 44	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (c e. t /\ d e. t)) -> (g` c) e. A)
46	45	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((c e. t /\ d e. t) /\ (a = (g` c) /\ b = (g` d) /\ c e. d))) -> (g` c) e. A)
47	40, 46	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((c e. t /\ d e. t) /\ (a = (g` c) /\ b = (g` d) /\ c e. d))) -> a e. A)
48		simprr2 925	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((c e. t /\ d e. t) /\ (a = (g` c) /\ b = (g` d) /\ c e. d))) -> b = (g` d))
49		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((g:t-->A /\ d e. t) -> (g` d) e. A)
50	49, 34	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((g:t-1-1->A /\ d e. t) -> (g` d) e. A)
51	50	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((A e. B /\ g:t-1-1->A) /\ d e. t) -> (g` d) e. A)
52	51	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (c e. t /\ d e. t)) -> (g` d) e. A)
53	52	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((c e. t /\ d e. t) /\ (a = (g` c) /\ b = (g` d) /\ c e. d))) -> (g` d) e. A)
54	48, 53	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((c e. t /\ d e. t) /\ (a = (g` c) /\ b = (g` d) /\ c e. d))) -> b e. A)
55		opelxpi 4040	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((a e. A /\ b e. A) -> <.a, b>. e. (A X. A))
56	47, 54, 55	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((c e. t /\ d e. t) /\ (a = (g` c) /\ b = (g` d) /\ c e. d))) -> <.a, b>. e. (A X. A))
57	56	exp32 408	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> ((c e. t /\ d e. t) -> ((a = (g` c) /\ b = (g` d) /\ c e. d) -> <.a, b>. e. (A X. A))))
58	57	r19.23advv 2218	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> (E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d) -> <.a, b>. e. (A X. A)))
59	58	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)) -> <.a, b>. e. (A X. A))
60	59	adantrl 430	. . . . . . . . . . . . . . . . . . . . 21 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (m = <.a, b>. /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d))) -> <.a, b>. e. (A X. A))
61	39, 60	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . 20 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ (m = <.a, b>. /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d))) -> m e. (A X. A))
62	61	ex 402	. . . . . . . . . . . . . . . . . . 19 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> ((m = <.a, b>. /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)) -> m e. (A X. A)))
63	62	19.23advv 1676	. . . . . . . . . . . . . . . . . 18 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> (E.aE.b(m = <.a, b>. /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)) -> m e. (A X. A)))
64		elopab 3559	. . . . . . . . . . . . . . . . . 18 |- (m e. {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} <-> E.aE.b(m = <.a, b>. /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)))
65	63, 64	syl5ib 223	. . . . . . . . . . . . . . . . 17 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> (m e. {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> m e. (A X. A)))
66	65	ssrdv 2622	. . . . . . . . . . . . . . . 16 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A))
67		eloni 3667	. . . . . . . . . . . . . . . . . . 19 |- (t e. On -> Ord t)
68		ordwe 3671	. . . . . . . . . . . . . . . . . . 19 |- (Ord t -> _E We t)
69	67, 68	syl 12	. . . . . . . . . . . . . . . . . 18 |- (t e. On -> _E We t)
70	69	adantl 424	. . . . . . . . . . . . . . . . 17 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> _E We t)
71		eqid 1884	. . . . . . . . . . . . . . . . . . 19 |- {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}
72	20, 71	hartoglem 5692	. . . . . . . . . . . . . . . . . 18 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> g Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)))
73		isowe 4880	. . . . . . . . . . . . . . . . . 18 |- (g Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)) -> ( _E We t <-> {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)))
74	72, 73	syl 12	. . . . . . . . . . . . . . . . 17 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> ( _E We t <-> {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)))
75	70, 74	mpbid 212	. . . . . . . . . . . . . . . 16 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))
76	38, 66, 75	3jca 1050	. . . . . . . . . . . . . . 15 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)))
77	72	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> g Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)))
78		visset 2295	. . . . . . . . . . . . . . . . . . . 20 |- g e. _V
79		isoeq1 4863	. . . . . . . . . . . . . . . . . . . 20 |- (f = g -> (f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)) <-> g Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t))))
80	78, 79	cla4ev 2371	. . . . . . . . . . . . . . . . . . 19 |- (g Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)) -> E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)))
81	77, 80	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)))
82		simplr 449	. . . . . . . . . . . . . . . . . . 19 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> t e. On)
83		imaexg 4279	. . . . . . . . . . . . . . . . . . . . . 22 |- (g e. _V -> (g"t) e. _V)
84	78, 83	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21 |- (g"t) e. _V
85	84	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> (g"t) e. _V)
86		simp3 878	. . . . . . . . . . . . . . . . . . . . 21 |- (((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) -> {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))
87	86	adantl 424	. . . . . . . . . . . . . . . . . . . 20 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))
88		ordtype 5691	. . . . . . . . . . . . . . . . . . . 20 |- (((g"t) e. _V /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) -> E!o e. On E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t)))
89	85, 87, 88	syl11anc 524	. . . . . . . . . . . . . . . . . . 19 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> E!o e. On E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t)))
90		isoeq4 4866	. . . . . . . . . . . . . . . . . . . . 21 |- (o = t -> (f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t)) <-> f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t))))
91	90	exbidv 1657	. . . . . . . . . . . . . . . . . . . 20 |- (o = t -> (E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t)) <-> E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t))))
92	91	reuuni2 3811	. . . . . . . . . . . . . . . . . . 19 |- ((t e. On /\ E!o e. On E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))) -> (E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)) <-> U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))} = t))
93	82, 89, 92	syl11anc 524	. . . . . . . . . . . . . . . . . 18 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> (E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (t, (g"t)) <-> U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))} = t))
94	81, 93	mpbid 212	. . . . . . . . . . . . . . . . 17 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))} = t)
95	94	eqcomd 1889	. . . . . . . . . . . . . . . 16 |- ((((A e. B /\ g:t-1-1->A) /\ t e. On) /\ ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))) -> t = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))})
96	95	ex 402	. . . . . . . . . . . . . . 15 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> (((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) -> t = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))}))
97	76, 96	jcai 313	. . . . . . . . . . . . . 14 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> (((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) /\ t = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))}))
98		visset 2295	. . . . . . . . . . . . . . . . 17 |- t e. _V
99	98	abrexex 4836	. . . . . . . . . . . . . . . . 17 |- {m | E.d e. t m = <.(g` c), (g` d)>.} e. _V
100	98, 99	abrexex2 4847	. . . . . . . . . . . . . . . 16 |- {m | E.c e. t E.d e. t m = <.(g` c), (g` d)>.} e. _V
101		ssab 2677	. . . . . . . . . . . . . . . . 17 |- ({<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ {m | E.c e. t E.d e. t m = <.(g` c), (g` d)>.} <-> A.m(m e. {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> E.c e. t E.d e. t m = <.(g` c), (g` d)>.))
102		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . 23 |- (m = <.a, b>. -> (m = <.(g` c), (g` d)>. <-> <.a, b>. = <.(g` c), (g` d)>.))
103		opeq12 3160	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((a = (g` c) /\ b = (g` d)) -> <.a, b>. = <.(g` c), (g` d)>.)
104	103	3adant3 896	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((a = (g` c) /\ b = (g` d) /\ c e. d) -> <.a, b>. = <.(g` c), (g` d)>.)
105	102, 104	syl5bir 227	. . . . . . . . . . . . . . . . . . . . . 22 |- (m = <.a, b>. -> ((a = (g` c) /\ b = (g` d) /\ c e. d) -> m = <.(g` c), (g` d)>.))
106	105	reximdv 2202	. . . . . . . . . . . . . . . . . . . . 21 |- (m = <.a, b>. -> (E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d) -> E.d e. t m = <.(g` c), (g` d)>.))
107	106	reximdv 2202	. . . . . . . . . . . . . . . . . . . 20 |- (m = <.a, b>. -> (E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d) -> E.c e. t E.d e. t m = <.(g` c), (g` d)>.))
108	107	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((m = <.a, b>. /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)) -> E.c e. t E.d e. t m = <.(g` c), (g` d)>.)
109	108	19.23aivv 1675	. . . . . . . . . . . . . . . . . 18 |- (E.aE.b(m = <.a, b>. /\ E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)) -> E.c e. t E.d e. t m = <.(g` c), (g` d)>.)
110	64, 109	sylbi 216	. . . . . . . . . . . . . . . . 17 |- (m e. {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> E.c e. t E.d e. t m = <.(g` c), (g` d)>.)
111	101, 110	mpgbir 1334	. . . . . . . . . . . . . . . 16 |- {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ {m | E.c e. t E.d e. t m = <.(g` c), (g` d)>.}
112	100, 111	ssexi 3456	. . . . . . . . . . . . . . 15 |- {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} e. _V
113		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (y = (g"t) -> (y C_ A <-> (g"t) C_ A))
114		weeq2 3647	. . . . . . . . . . . . . . . . . 18 |- (y = (g"t) -> (w We y <-> w We (g"t)))
115	113, 114	3anbi13d 1170	. . . . . . . . . . . . . . . . 17 |- (y = (g"t) -> ((y C_ A /\ w C_ (A X. A) /\ w We y) <-> ((g"t) C_ A /\ w C_ (A X. A) /\ w We (g"t))))
116		isoeq5 4867	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (g"t) -> (f Isom _E , w (o, y) <-> f Isom _E , w (o, (g"t))))
117	116	exbidv 1657	. . . . . . . . . . . . . . . . . . . 20 |- (y = (g"t) -> (E.f f Isom _E , w (o, y) <-> E.f f Isom _E , w (o, (g"t))))
118	117	rabbidv 2287	. . . . . . . . . . . . . . . . . . 19 |- (y = (g"t) -> {o e. On | E.f f Isom _E , w (o, y)} = {o e. On | E.f f Isom _E , w (o, (g"t))})
119	118	unieqd 3188	. . . . . . . . . . . . . . . . . 18 |- (y = (g"t) -> U.{o e. On | E.f f Isom _E , w (o, y)} = U.{o e. On | E.f f Isom _E , w (o, (g"t))})
120	119	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (y = (g"t) -> (z = U.{o e. On | E.f f Isom _E , w (o, y)} <-> z = U.{o e. On | E.f f Isom _E , w (o, (g"t))}))
121	115, 120	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (y = (g"t) -> (((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)}) <-> (((g"t) C_ A /\ w C_ (A X. A) /\ w We (g"t)) /\ z = U.{o e. On | E.f f Isom _E , w (o, (g"t))})))
122		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> (w C_ (A X. A) <-> {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A)))
123		weeq1 3646	. . . . . . . . . . . . . . . . . 18 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> (w We (g"t) <-> {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)))
124	122, 123	3anbi23d 1171	. . . . . . . . . . . . . . . . 17 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> (((g"t) C_ A /\ w C_ (A X. A) /\ w We (g"t)) <-> ((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t))))
125		isoeq3 4865	. . . . . . . . . . . . . . . . . . . . 21 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> (f Isom _E , w (o, (g"t)) <-> f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))))
126	125	exbidv 1657	. . . . . . . . . . . . . . . . . . . 20 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> (E.f f Isom _E , w (o, (g"t)) <-> E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))))
127	126	rabbidv 2287	. . . . . . . . . . . . . . . . . . 19 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> {o e. On | E.f f Isom _E , w (o, (g"t))} = {o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))})
128	127	unieqd 3188	. . . . . . . . . . . . . . . . . 18 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> U.{o e. On | E.f f Isom _E , w (o, (g"t))} = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))})
129	128	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> (z = U.{o e. On | E.f f Isom _E , w (o, (g"t))} <-> z = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))}))
130	124, 129	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (w = {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} -> ((((g"t) C_ A /\ w C_ (A X. A) /\ w We (g"t)) /\ z = U.{o e. On | E.f f Isom _E , w (o, (g"t))}) <-> (((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) /\ z = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))})))
131		eqeq1 1890	. . . . . . . . . . . . . . . . 17 |- (z = t -> (z = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))} <-> t = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))}))
132	131	anbi2d 678	. . . . . . . . . . . . . . . 16 |- (z = t -> ((((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) /\ z = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))}) <-> (((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) /\ t = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))})))
133	121, 130, 132	eloprabg 4936	. . . . . . . . . . . . . . 15 |- (((g"t) e. _V /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} e. _V /\ t e. _V) -> (<.<.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>., t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} <-> (((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) /\ t = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))})))
134	84, 112, 98, 133	mp3an 1191	. . . . . . . . . . . . . 14 |- (<.<.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>., t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} <-> (((g"t) C_ A /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} C_ (A X. A) /\ {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} We (g"t)) /\ t = U.{o e. On | E.f f Isom _E , {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)} (o, (g"t))}))
135	97, 134	sylibr 217	. . . . . . . . . . . . 13 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> <.<.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>., t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})
136		opex 3527	. . . . . . . . . . . . . 14 |- <.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>. e. _V
137		opeq1 3158	. . . . . . . . . . . . . . 15 |- (p = <.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>. -> <.p, t>. = <.<.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>., t>.)
138	137	eleq1d 1963	. . . . . . . . . . . . . 14 |- (p = <.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>. -> (<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} <-> <.<.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>., t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})}))
139	136, 138	cla4ev 2371	. . . . . . . . . . . . 13 |- (<.<.(g"t), {<.a, b>. | E.c e. t E.d e. t (a = (g` c) /\ b = (g` d) /\ c e. d)}>., t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} -> E.p<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})
140	135, 139	syl 12	. . . . . . . . . . . 12 |- (((A e. B /\ g:t-1-1->A) /\ t e. On) -> E.p<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})
141	140	exp31 407	. . . . . . . . . . 11 |- (A e. B -> (g:t-1-1->A -> (t e. On -> E.p<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})))
142	141	19.23adv 1584	. . . . . . . . . 10 |- (A e. B -> (E.g g:t-1-1->A -> (t e. On -> E.p<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})))
143	31, 142	sylbid 220	. . . . . . . . 9 |- (A e. B -> (t ~<_ A -> (t e. On -> E.p<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})))
144	143	com23 36	. . . . . . . 8 |- (A e. B -> (t e. On -> (t ~<_ A -> E.p<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})))
145	144	imp3a 388	. . . . . . 7 |- (A e. B -> ((t e. On /\ t ~<_ A) -> E.p<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})}))
146		breq1 3341	. . . . . . . 8 |- (x = t -> (x ~<_ A <-> t ~<_ A))
147	146	elrab 2414	. . . . . . 7 |- (t e. {x e. On | x ~<_ A} <-> (t e. On /\ t ~<_ A))
148	98	elrn2 4196	. . . . . . 7 |- (t e. ran {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} <-> E.p<.p, t>. e. {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})
149	145, 147, 148	3imtr4g 612	. . . . . 6 |- (A e. B -> (t e. {x e. On | x ~<_ A} -> t e. ran {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})}))
150	149	ssrdv 2622	. . . . 5 |- (A e. B -> {x e. On | x ~<_ A} C_ ran {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})})
151		ordtype 5691	. . . . . . . . . . . . . . 15 |- ((y e. _V /\ w We y) -> E!o e. On E.f f Isom _E , w (o, y))
152	9, 151	mpan 759	. . . . . . . . . . . . . 14 |- (w We y -> E!o e. On E.f f Isom _E , w (o, y))
153	152	3ad2ant3 899	. . . . . . . . . . . . 13 |- ((y C_ A /\ w C_ (A X. A) /\ w We y) -> E!o e. On E.f f Isom _E , w (o, y))
154	153	adantl 424	. . . . . . . . . . . 12 |- ((A e. B /\ (y C_ A /\ w C_ (A X. A) /\ w We y)) -> E!o e. On E.f f Isom _E , w (o, y))
155		reucl 3213	. . . . . . . . . . . 12 |- (E!o e. On E.f f Isom _E , w (o, y) -> U.{o e. On | E.f f Isom _E , w (o, y)} e. On)
156		elisset 2299	. . . . . . . . . . . 12 |- (U.{o e. On | E.f f Isom _E , w (o, y)} e. On -> U.{o e. On | E.f f Isom _E , w (o, y)} e. _V)
157	154, 155, 156	3syl 24	. . . . . . . . . . 11 |- ((A e. B /\ (y C_ A /\ w C_ (A X. A) /\ w We y)) -> U.{o e. On | E.f f Isom _E , w (o, y)} e. _V)
158		eueq 2427	. . . . . . . . . . 11 |- (U.{o e. On | E.f f Isom _E , w (o, y)} e. _V <-> E!z z = U.{o e. On | E.f f Isom _E , w (o, y)})
159	157, 158	sylib 215	. . . . . . . . . 10 |- ((A e. B /\ (y C_ A /\ w C_ (A X. A) /\ w We y)) -> E!z z = U.{o e. On | E.f f Isom _E , w (o, y)})
160	159	ex 402	. . . . . . . . 9 |- (A e. B -> ((y C_ A /\ w C_ (A X. A) /\ w We y) -> E!z z = U.{o e. On | E.f f Isom _E , w (o, y)}))
161	160	19.21aivv 1665	. . . . . . . 8 |- (A e. B -> A.yA.w((y C_ A /\ w C_ (A X. A) /\ w We y) -> E!z z = U.{o e. On | E.f f Isom _E , w (o, y)}))
162		fnoprabg 4941	. . . . . . . 8 |- (A.yA.w((y C_ A /\ w C_ (A X. A) /\ w We y) -> E!z z = U.{o e. On | E.f f Isom _E , w (o, y)}) -> {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} Fn {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)})
163		fndm 4512	. . . . . . . 8 |- ({<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} Fn {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)} -> dom {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} = {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)})
164	161, 162, 163	3syl 24	. . . . . . 7 |- (A e. B -> dom {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} = {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)})
165		elopab 3559	. . . . . . . . . . 11 |- (t e. {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)} <-> E.yE.w(t = <.y, w>. /\ (y C_ A /\ w C_ (A X. A) /\ w We y)))
166		simpl 346	. . . . . . . . . . . . 13 |- ((t = <.y, w>. /\ (y C_ A /\ w C_ (A X. A) /\ w We y)) -> t = <.y, w>.)
167		opelxpi 4040	. . . . . . . . . . . . . . . 16 |- ((y e. ~PA /\ w e. ~P(A X. A)) -> <.y, w>. e. (~PA X. ~P(A X. A)))
168	9	elpw 3037	. . . . . . . . . . . . . . . 16 |- (y e. ~PA <-> y C_ A)
169		visset 2295	. . . . . . . . . . . . . . . . 17 |- w e. _V
170	169	elpw 3037	. . . . . . . . . . . . . . . 16 |- (w e. ~P(A X. A) <-> w C_ (A X. A))
171	167, 168, 170	syl2anbr 505	. . . . . . . . . . . . . . 15 |- ((y C_ A /\ w C_ (A X. A)) -> <.y, w>. e. (~PA X. ~P(A X. A)))
172	171	3adant3 896	. . . . . . . . . . . . . 14 |- ((y C_ A /\ w C_ (A X. A) /\ w We y) -> <.y, w>. e. (~PA X. ~P(A X. A)))
173	172	adantl 424	. . . . . . . . . . . . 13 |- ((t = <.y, w>. /\ (y C_ A /\ w C_ (A X. A) /\ w We y)) -> <.y, w>. e. (~PA X. ~P(A X. A)))
174	166, 173	eqeltrd 1971	. . . . . . . . . . . 12 |- ((t = <.y, w>. /\ (y C_ A /\ w C_ (A X. A) /\ w We y)) -> t e. (~PA X. ~P(A X. A)))
175	174	19.23aivv 1675	. . . . . . . . . . 11 |- (E.yE.w(t = <.y, w>. /\ (y C_ A /\ w C_ (A X. A) /\ w We y)) -> t e. (~PA X. ~P(A X. A)))
176	165, 175	sylbi 216	. . . . . . . . . 10 |- (t e. {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)} -> t e. (~PA X. ~P(A X. A)))
177	176	ssriv 2621	. . . . . . . . 9 |- {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)} C_ (~PA X. ~P(A X. A))
178	177	a1i 8	. . . . . . . 8 |- (A e. B -> {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)} C_ (~PA X. ~P(A X. A)))
179		pwexg 3489	. . . . . . . . 9 |- (A e. B -> ~PA e. _V)
180		xpexg 4095	. . . . . . . . . . 11 |- ((A e. B /\ A e. B) -> (A X. A) e. _V)
181	180	anidms 480	. . . . . . . . . 10 |- (A e. B -> (A X. A) e. _V)
182		pwexg 3489	. . . . . . . . . 10 |- ((A X. A) e. _V -> ~P(A X. A) e. _V)
183	181, 182	syl 12	. . . . . . . . 9 |- (A e. B -> ~P(A X. A) e. _V)
184		xpexg 4095	. . . . . . . . 9 |- ((~PA e. _V /\ ~P(A X. A) e. _V) -> (~PA X. ~P(A X. A)) e. _V)
185	179, 183, 184	syl11anc 524	. . . . . . . 8 |- (A e. B -> (~PA X. ~P(A X. A)) e. _V)
186		ssexg 3457	. . . . . . . 8 |- (({<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)} C_ (~PA X. ~P(A X. A)) /\ (~PA X. ~P(A X. A)) e. _V) -> {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)} e. _V)
187	178, 185, 186	syl11anc 524	. . . . . . 7 |- (A e. B -> {<.y, w>. | (y C_ A /\ w C_ (A X. A) /\ w We y)} e. _V)
188	164, 187	eqeltrd 1971	. . . . . 6 |- (A e. B -> dom {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} e. _V)
189		moeq 2431	. . . . . . . . 9 |- E*z z = U.{o e. On | E.f f Isom _E , w (o, y)}
190	189	moani 1820	. . . . . . . 8 |- E*z((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})
191	190	funoprab 4940	. . . . . . 7 |- Fun {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})}
192		funrnex 4544	. . . . . . 7 |- (dom {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} e. _V -> (Fun {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} -> ran {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} e. _V))
193	191, 192	mpi 55	. . . . . 6 |- (dom {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} e. _V -> ran {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} e. _V)
194	188, 193	syl 12	. . . . 5 |- (A e. B -> ran {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} e. _V)
195		ssexg 3457	. . . . 5 |- (({x e. On | x ~<_ A} C_ ran {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} /\ ran {<.<.y, w>., z>. | ((y C_ A /\ w C_ (A X. A) /\ w We y) /\ z = U.{o e. On | E.f f Isom _E , w (o, y)})} e. _V) -> {x e. On | x ~<_ A} e. _V)
196	150, 194, 195	syl11anc 524	. . . 4 |- (A e. B -> {x e. On | x ~<_ A} e. _V)
197	196, 20	syl5eqel 1975	. . 3 |- (A e. B -> H e. _V)
198		elong 3665	. . 3 |- (H e. _V -> (H e. On <-> Ord H))
199	197, 198	syl 12	. 2 |- (A e. B -> (H e. On <-> Ord H))
200	30, 199	mpbiri 211	1 |- (A e. B -> H e. On)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  {cab 1871  E.wrex 2106  E!wreu 2107  {crab 2108  _Vcvv 2292   C_ wss 2593  ~Pcpw 3032  <.cop 3046  U.cuni 3177   class class class wbr 3338  {copab 3395  Tr wtr 3411   _E cep 3581   We wwe 3624  Ord word 3656  Oncon0 3657   X. cxp 3984  dom cdm 3986  ran crn 3987  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  ` cfv 3998   Isom wiso 3999  {copab2 4885   ~<_ cdom 5424

This theorem is referenced by:  onsdom 5694  onsdomOLD 15385

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-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  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-iun 3257  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-suc 3663  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  df-oprab 4887  df-en 5427  df-dom 5428

Copyright terms: Public domain