Theorem infxpenlem 7851

Description: Lemma for infxpen 7852. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)

Hypotheses

Ref	Expression
leweon.1	|- L = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
r0weon.1	|- R = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) }
infxpen.1	|- Q = ( R i^i ( ( a X. a ) X. ( a X. a ) ) )
infxpen.2	|- ( ph <-> ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) )
infxpen.3	|- M = ( ( 1st ` w ) u. ( 2nd ` w ) )
infxpen.4	|- J = OrdIso ( Q , ( a X. a ) )

Assertion

Ref	Expression
infxpenlem	|- ( ( A e. On /\ om C_ A ) -> ( A X. A ) ~~ A )

Distinct variable groups:   A, a   w, J   z, w, L   z, m, M   ph, w, z   z, Q   m, a, w, x, y, z

Allowed substitution hints:   ph( x, y, m, a)   A( x, y, z, w, m)   Q( x, y, w, m, a)   R( x, y, z, w, m, a)   J( x, y, z, m, a)   L( x, y, m, a)   M( x, y, w, a)

Proof of Theorem infxpenlem

Step	Hyp	Ref	Expression
1		sseq2 3330	. . . 4 |- ( a = m -> ( om C_ a <-> om C_ m ) )
2		xpeq12 4856	. . . . . 6 |- ( ( a = m /\ a = m ) -> ( a X. a ) = ( m X. m ) )
3	2	anidms 627	. . . . 5 |- ( a = m -> ( a X. a ) = ( m X. m ) )
4		id 20	. . . . 5 |- ( a = m -> a = m )
5	3, 4	breq12d 4185	. . . 4 |- ( a = m -> ( ( a X. a ) ~~ a <-> ( m X. m ) ~~ m ) )
6	1, 5	imbi12d 312	. . 3 |- ( a = m -> ( ( om C_ a -> ( a X. a ) ~~ a ) <-> ( om C_ m -> ( m X. m ) ~~ m ) ) )
7		sseq2 3330	. . . 4 |- ( a = A -> ( om C_ a <-> om C_ A ) )
8		xpeq12 4856	. . . . . 6 |- ( ( a = A /\ a = A ) -> ( a X. a ) = ( A X. A ) )
9	8	anidms 627	. . . . 5 |- ( a = A -> ( a X. a ) = ( A X. A ) )
10		id 20	. . . . 5 |- ( a = A -> a = A )
11	9, 10	breq12d 4185	. . . 4 |- ( a = A -> ( ( a X. a ) ~~ a <-> ( A X. A ) ~~ A ) )
12	7, 11	imbi12d 312	. . 3 |- ( a = A -> ( ( om C_ a -> ( a X. a ) ~~ a ) <-> ( om C_ A -> ( A X. A ) ~~ A ) ) )
13		infxpen.2	. . . . . . . 8 |- ( ph <-> ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) )
14		vex 2919	. . . . . . . . . . . . . 14 |- a e. _V
15	14, 14	xpex 4949	. . . . . . . . . . . . 13 |- ( a X. a ) e. _V
16		simpll 731	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) -> a e. On )
17	13, 16	sylbi 188	. . . . . . . . . . . . . . . . . 18 |- ( ph -> a e. On )
18		onss 4730	. . . . . . . . . . . . . . . . . 18 |- ( a e. On -> a C_ On )
19	17, 18	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> a C_ On )
20		xpss12 4940	. . . . . . . . . . . . . . . . 17 |- ( ( a C_ On /\ a C_ On ) -> ( a X. a ) C_ ( On X. On ) )
21	19, 19, 20	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ph -> ( a X. a ) C_ ( On X. On ) )
22		leweon.1	. . . . . . . . . . . . . . . . . 18 |- L = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
23		r0weon.1	. . . . . . . . . . . . . . . . . 18 |- R = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) }
24	22, 23	r0weon 7850	. . . . . . . . . . . . . . . . 17 |- ( R We ( On X. On ) /\ R Se ( On X. On ) )
25	24	simpli 445	. . . . . . . . . . . . . . . 16 |- R We ( On X. On )
26		wess 4529	. . . . . . . . . . . . . . . 16 |- ( ( a X. a ) C_ ( On X. On ) -> ( R We ( On X. On ) -> R We ( a X. a ) ) )
27	21, 25, 26	ee10 1382	. . . . . . . . . . . . . . 15 |- ( ph -> R We ( a X. a ) )
28		weinxp 4904	. . . . . . . . . . . . . . 15 |- ( R We ( a X. a ) <-> ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) We ( a X. a ) )
29	27, 28	sylib 189	. . . . . . . . . . . . . 14 |- ( ph -> ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) We ( a X. a ) )
30		infxpen.1	. . . . . . . . . . . . . . 15 |- Q = ( R i^i ( ( a X. a ) X. ( a X. a ) ) )
31		weeq1 4530	. . . . . . . . . . . . . . 15 |- ( Q = ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) -> ( Q We ( a X. a ) <-> ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) We ( a X. a ) ) )
32	30, 31	ax-mp 8	. . . . . . . . . . . . . 14 |- ( Q We ( a X. a ) <-> ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) We ( a X. a ) )
33	29, 32	sylibr 204	. . . . . . . . . . . . 13 |- ( ph -> Q We ( a X. a ) )
34		infxpen.4	. . . . . . . . . . . . . 14 |- J = OrdIso ( Q , ( a X. a ) )
35	34	oiiso 7462	. . . . . . . . . . . . 13 |- ( ( ( a X. a ) e. _V /\ Q We ( a X. a ) ) -> J Isom _E , Q ( dom J , ( a X. a ) ) )
36	15, 33, 35	sylancr 645	. . . . . . . . . . . 12 |- ( ph -> J Isom _E , Q ( dom J , ( a X. a ) ) )
37		isof1o 6004	. . . . . . . . . . . 12 |- ( J Isom _E , Q ( dom J , ( a X. a ) ) -> J : dom J -1-1-onto-> ( a X. a ) )
38	36, 37	syl 16	. . . . . . . . . . 11 |- ( ph -> J : dom J -1-1-onto-> ( a X. a ) )
39		f1ocnv 5646	. . . . . . . . . . 11 |- ( J : dom J -1-1-onto-> ( a X. a ) -> `' J : ( a X. a ) -1-1-onto-> dom J )
40		f1of1 5632	. . . . . . . . . . 11 |- ( `' J : ( a X. a ) -1-1-onto-> dom J -> `' J : ( a X. a ) -1-1-> dom J )
41	38, 39, 40	3syl 19	. . . . . . . . . 10 |- ( ph -> `' J : ( a X. a ) -1-1-> dom J )
42		f1f1orn 5644	. . . . . . . . . 10 |- ( `' J : ( a X. a ) -1-1-> dom J -> `' J : ( a X. a ) -1-1-onto-> ran `' J )
43	15	f1oen 7087	. . . . . . . . . 10 |- ( `' J : ( a X. a ) -1-1-onto-> ran `' J -> ( a X. a ) ~~ ran `' J )
44	41, 42, 43	3syl 19	. . . . . . . . 9 |- ( ph -> ( a X. a ) ~~ ran `' J )
45		f1ofn 5634	. . . . . . . . . . 11 |- ( `' J : ( a X. a ) -1-1-onto-> dom J -> `' J Fn ( a X. a ) )
46	38, 39, 45	3syl 19	. . . . . . . . . 10 |- ( ph -> `' J Fn ( a X. a ) )
47	36	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. ( a X. a ) ) -> J Isom _E , Q ( dom J , ( a X. a ) ) )
48	37, 39, 40	3syl 19	. . . . . . . . . . . . . . . . . 18 |- ( J Isom _E , Q ( dom J , ( a X. a ) ) -> `' J : ( a X. a ) -1-1-> dom J )
49		cnvimass 5183	. . . . . . . . . . . . . . . . . . 19 |- ( `' Q " { w } ) C_ dom Q
50		inss2 3522	. . . . . . . . . . . . . . . . . . . . . 22 |- ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) C_ ( ( a X. a ) X. ( a X. a ) )
51	30, 50	eqsstri 3338	. . . . . . . . . . . . . . . . . . . . 21 |- Q C_ ( ( a X. a ) X. ( a X. a ) )
52		dmss 5028	. . . . . . . . . . . . . . . . . . . . 21 |- ( Q C_ ( ( a X. a ) X. ( a X. a ) ) -> dom Q C_ dom ( ( a X. a ) X. ( a X. a ) ) )
53	51, 52	ax-mp 8	. . . . . . . . . . . . . . . . . . . 20 |- dom Q C_ dom ( ( a X. a ) X. ( a X. a ) )
54		dmxpid 5048	. . . . . . . . . . . . . . . . . . . 20 |- dom ( ( a X. a ) X. ( a X. a ) ) = ( a X. a )
55	53, 54	sseqtri 3340	. . . . . . . . . . . . . . . . . . 19 |- dom Q C_ ( a X. a )
56	49, 55	sstri 3317	. . . . . . . . . . . . . . . . . 18 |- ( `' Q " { w } ) C_ ( a X. a )
57		f1ores 5648	. . . . . . . . . . . . . . . . . 18 |- ( ( `' J : ( a X. a ) -1-1-> dom J /\ ( `' Q " { w } ) C_ ( a X. a ) ) -> ( `' J |` ( `' Q " { w } ) ) : ( `' Q " { w } ) -1-1-onto-> ( `' J " ( `' Q " { w } ) ) )
58	48, 56, 57	sylancl 644	. . . . . . . . . . . . . . . . 17 |- ( J Isom _E , Q ( dom J , ( a X. a ) ) -> ( `' J |` ( `' Q " { w } ) ) : ( `' Q " { w } ) -1-1-onto-> ( `' J " ( `' Q " { w } ) ) )
59	15, 15	xpex 4949	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a X. a ) X. ( a X. a ) ) e. _V
60	59	inex2 4305	. . . . . . . . . . . . . . . . . . . . 21 |- ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) e. _V
61	30, 60	eqeltri 2474	. . . . . . . . . . . . . . . . . . . 20 |- Q e. _V
62	61	cnvex 5365	. . . . . . . . . . . . . . . . . . 19 |- `' Q e. _V
63		imaexg 5176	. . . . . . . . . . . . . . . . . . 19 |- ( `' Q e. _V -> ( `' Q " { w } ) e. _V )
64	62, 63	ax-mp 8	. . . . . . . . . . . . . . . . . 18 |- ( `' Q " { w } ) e. _V
65	64	f1oen 7087	. . . . . . . . . . . . . . . . 17 |- ( ( `' J |` ( `' Q " { w } ) ) : ( `' Q " { w } ) -1-1-onto-> ( `' J " ( `' Q " { w } ) ) -> ( `' Q " { w } ) ~~ ( `' J " ( `' Q " { w } ) ) )
66	47, 58, 65	3syl 19	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) ~~ ( `' J " ( `' Q " { w } ) ) )
67		sseqin2 3520	. . . . . . . . . . . . . . . . . . 19 |- ( ( `' Q " { w } ) C_ ( a X. a ) <-> ( ( a X. a ) i^i ( `' Q " { w } ) ) = ( `' Q " { w } ) )
68	56, 67	mpbi 200	. . . . . . . . . . . . . . . . . 18 |- ( ( a X. a ) i^i ( `' Q " { w } ) ) = ( `' Q " { w } )
69	68	imaeq2i 5160	. . . . . . . . . . . . . . . . 17 |- ( `' J " ( ( a X. a ) i^i ( `' Q " { w } ) ) ) = ( `' J " ( `' Q " { w } ) )
70		isocnv 6009	. . . . . . . . . . . . . . . . . . . 20 |- ( J Isom _E , Q ( dom J , ( a X. a ) ) -> `' J Isom Q , _E ( ( a X. a ) , dom J ) )
71	47, 70	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. ( a X. a ) ) -> `' J Isom Q , _E ( ( a X. a ) , dom J ) )
72		simpr 448	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. ( a X. a ) ) -> w e. ( a X. a ) )
73		isoini 6017	. . . . . . . . . . . . . . . . . . 19 |- ( ( `' J Isom Q , _E ( ( a X. a ) , dom J ) /\ w e. ( a X. a ) ) -> ( `' J " ( ( a X. a ) i^i ( `' Q " { w } ) ) ) = ( dom J i^i ( `' _E " { ( `' J ` w ) } ) ) )
74	71, 72, 73	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J " ( ( a X. a ) i^i ( `' Q " { w } ) ) ) = ( dom J i^i ( `' _E " { ( `' J ` w ) } ) ) )
75		fvex 5701	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' J ` w ) e. _V
76	75	epini 5193	. . . . . . . . . . . . . . . . . . . 20 |- ( `' _E " { ( `' J ` w ) } ) = ( `' J ` w )
77	76	ineq2i 3499	. . . . . . . . . . . . . . . . . . 19 |- ( dom J i^i ( `' _E " { ( `' J ` w ) } ) ) = ( dom J i^i ( `' J ` w ) )
78	34	oicl 7454	. . . . . . . . . . . . . . . . . . . . 21 |- Ord dom J
79	37, 39	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( J Isom _E , Q ( dom J , ( a X. a ) ) -> `' J : ( a X. a ) -1-1-onto-> dom J )
80		f1of 5633	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( `' J : ( a X. a ) -1-1-onto-> dom J -> `' J : ( a X. a ) --> dom J )
81	36, 79, 80	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> `' J : ( a X. a ) --> dom J )
82	81	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) e. dom J )
83		ordelss 4557	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Ord dom J /\ ( `' J ` w ) e. dom J ) -> ( `' J ` w ) C_ dom J )
84	78, 82, 83	sylancr 645	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) C_ dom J )
85		dfss1 3505	. . . . . . . . . . . . . . . . . . . 20 |- ( ( `' J ` w ) C_ dom J <-> ( dom J i^i ( `' J ` w ) ) = ( `' J ` w ) )
86	84, 85	sylib 189	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. ( a X. a ) ) -> ( dom J i^i ( `' J ` w ) ) = ( `' J ` w ) )
87	77, 86	syl5eq 2448	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w e. ( a X. a ) ) -> ( dom J i^i ( `' _E " { ( `' J ` w ) } ) ) = ( `' J ` w ) )
88	74, 87	eqtrd 2436	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J " ( ( a X. a ) i^i ( `' Q " { w } ) ) ) = ( `' J ` w ) )
89	69, 88	syl5eqr 2450	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J " ( `' Q " { w } ) ) = ( `' J ` w ) )
90	66, 89	breqtrd 4196	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) ~~ ( `' J ` w ) )
91	90	ensymd 7117	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) ~~ ( `' Q " { w } ) )
92		infxpen.3	. . . . . . . . . . . . . . . . . . 19 |- M = ( ( 1st ` w ) u. ( 2nd ` w ) )
93		fvex 5701	. . . . . . . . . . . . . . . . . . . 20 |- ( 1st ` w ) e. _V
94		fvex 5701	. . . . . . . . . . . . . . . . . . . 20 |- ( 2nd ` w ) e. _V
95	93, 94	unex 4666	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1st ` w ) u. ( 2nd ` w ) ) e. _V
96	92, 95	eqeltri 2474	. . . . . . . . . . . . . . . . . 18 |- M e. _V
97	96	sucex 4750	. . . . . . . . . . . . . . . . 17 |- suc M e. _V
98	97, 97	xpex 4949	. . . . . . . . . . . . . . . 16 |- ( suc M X. suc M ) e. _V
99		xpss 4941	. . . . . . . . . . . . . . . . . . . 20 |- ( a X. a ) C_ ( _V X. _V )
100		simp3 959	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z e. ( `' Q " { w } ) )
101		vex 2919	. . . . . . . . . . . . . . . . . . . . . . 23 |- w e. _V
102		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . 24 |- z e. _V
103	102	eliniseg 5192	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w e. _V -> ( z e. ( `' Q " { w } ) <-> z Q w ) )
104	101, 103	ax-mp 8	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( `' Q " { w } ) <-> z Q w )
105	100, 104	sylib 189	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z Q w )
106	30	breqi 4178	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z Q w <-> z ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) w )
107		brin 4219	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) w <-> ( z R w /\ z ( ( a X. a ) X. ( a X. a ) ) w ) )
108	106, 107	bitri 241	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z Q w <-> ( z R w /\ z ( ( a X. a ) X. ( a X. a ) ) w ) )
109	108	simprbi 451	. . . . . . . . . . . . . . . . . . . . 21 |- ( z Q w -> z ( ( a X. a ) X. ( a X. a ) ) w )
110		brxp 4868	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z ( ( a X. a ) X. ( a X. a ) ) w <-> ( z e. ( a X. a ) /\ w e. ( a X. a ) ) )
111	110	simplbi 447	. . . . . . . . . . . . . . . . . . . . 21 |- ( z ( ( a X. a ) X. ( a X. a ) ) w -> z e. ( a X. a ) )
112	105, 109, 111	3syl 19	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z e. ( a X. a ) )
113	99, 112	sseldi 3306	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z e. ( _V X. _V ) )
114	17	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. ( a X. a ) ) -> a e. On )
115	114	3adant3 977	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> a e. On )
116		xp1st 6335	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( a X. a ) -> ( 1st ` z ) e. a )
117		onelon 4566	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. On /\ ( 1st ` z ) e. a ) -> ( 1st ` z ) e. On )
118	116, 117	sylan2 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( a e. On /\ z e. ( a X. a ) ) -> ( 1st ` z ) e. On )
119	115, 112, 118	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 1st ` z ) e. On )
120		eloni 4551	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( a e. On -> Ord a )
121		elxp7 6338	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w e. ( a X. a ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. a /\ ( 2nd ` w ) e. a ) ) )
122	121	simprbi 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( w e. ( a X. a ) -> ( ( 1st ` w ) e. a /\ ( 2nd ` w ) e. a ) )
123		ordunel 4766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( Ord a /\ ( 1st ` w ) e. a /\ ( 2nd ` w ) e. a ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. a )
124	123	3expib 1156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( Ord a -> ( ( ( 1st ` w ) e. a /\ ( 2nd ` w ) e. a ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. a ) )
125	120, 122, 124	syl2im 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a e. On -> ( w e. ( a X. a ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. a ) )
126	114, 72, 125	sylc 58	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ w e. ( a X. a ) ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. a )
127	92, 126	syl5eqel 2488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ w e. ( a X. a ) ) -> M e. a )
128		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) -> A. m e. a m ~< a )
129	13, 128	sylbi 188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> A. m e. a m ~< a )
130		simprl 733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) -> om C_ a )
131	13, 130	sylbi 188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> om C_ a )
132		iscard 7818	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( card ` a ) = a <-> ( a e. On /\ A. m e. a m ~< a ) )
133		cardlim 7815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( om C_ ( card ` a ) <-> Lim ( card ` a ) )
134		sseq2 3330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( card ` a ) = a -> ( om C_ ( card ` a ) <-> om C_ a ) )
135		limeq 4553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( card ` a ) = a -> ( Lim ( card ` a ) <-> Lim a ) )
136	134, 135	bibi12d 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( card ` a ) = a -> ( ( om C_ ( card ` a ) <-> Lim ( card ` a ) ) <-> ( om C_ a <-> Lim a ) ) )
137	133, 136	mpbii 203	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( card ` a ) = a -> ( om C_ a <-> Lim a ) )
138	132, 137	sylbir 205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( a e. On /\ A. m e. a m ~< a ) -> ( om C_ a <-> Lim a ) )
139	138	biimpa 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( a e. On /\ A. m e. a m ~< a ) /\ om C_ a ) -> Lim a )
140	17, 129, 131, 139	syl21anc 1183	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> Lim a )
141	140	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ w e. ( a X. a ) ) -> Lim a )
142		limsuc 4788	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( Lim a -> ( M e. a <-> suc M e. a ) )
143	141, 142	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ w e. ( a X. a ) ) -> ( M e. a <-> suc M e. a ) )
144	127, 143	mpbid 202	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ w e. ( a X. a ) ) -> suc M e. a )
145		onelon 4566	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. On /\ suc M e. a ) -> suc M e. On )
146	114, 144, 145	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ w e. ( a X. a ) ) -> suc M e. On )
147	146	3adant3 977	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> suc M e. On )
148		ssun1 3470	. . . . . . . . . . . . . . . . . . . . 21 |- ( 1st ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) )
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 1st ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) ) )
150	108	simplbi 447	. . . . . . . . . . . . . . . . . . . . 21 |- ( z Q w -> z R w )
151		df-br 4173	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z R w <-> <. z , w >. e. R )
152	23	eleq2i 2468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( <. z , w >. e. R <-> <. z , w >. e. { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) } )
153		opabid 4421	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( <. z , w >. e. { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) } <-> ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) )
154	151, 152, 153	3bitri 263	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z R w <-> ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) ) )
155	154	simprbi 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z R w -> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) )
156		simpl 444	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) )
157	156	orim2i 505	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) ) -> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
158	155, 157	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z R w -> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
159		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 1st ` z ) e. _V
160		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2nd ` z ) e. _V
161	159, 160	unex 4666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 1st ` z ) u. ( 2nd ` z ) ) e. _V
162	161	elsuc 4610	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc ( ( 1st ` w ) u. ( 2nd ` w ) ) <-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
163	158, 162	sylibr 204	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z R w -> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc ( ( 1st ` w ) u. ( 2nd ` w ) ) )
164		suceq 4606	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( M = ( ( 1st ` w ) u. ( 2nd ` w ) ) -> suc M = suc ( ( 1st ` w ) u. ( 2nd ` w ) ) )
165	92, 164	ax-mp 8	. . . . . . . . . . . . . . . . . . . . . 22 |- suc M = suc ( ( 1st ` w ) u. ( 2nd ` w ) )
166	163, 165	syl6eleqr 2495	. . . . . . . . . . . . . . . . . . . . 21 |- ( z R w -> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc M )
167	105, 150, 166	3syl 19	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc M )
168		ontr2 4588	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 1st ` z ) e. On /\ suc M e. On ) -> ( ( ( 1st ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) ) /\ ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc M ) -> ( 1st ` z ) e. suc M ) )
169	168	imp 419	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 1st ` z ) e. On /\ suc M e. On ) /\ ( ( 1st ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) ) /\ ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc M ) ) -> ( 1st ` z ) e. suc M )
170	119, 147, 149, 167, 169	syl22anc 1185	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 1st ` z ) e. suc M )
171		xp2nd 6336	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( a X. a ) -> ( 2nd ` z ) e. a )
172		onelon 4566	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a e. On /\ ( 2nd ` z ) e. a ) -> ( 2nd ` z ) e. On )
173	171, 172	sylan2 461	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( a e. On /\ z e. ( a X. a ) ) -> ( 2nd ` z ) e. On )
174	115, 112, 173	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 2nd ` z ) e. On )
175		ssun2 3471	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2nd ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) )
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 2nd ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) ) )
177		ontr2 4588	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 2nd ` z ) e. On /\ suc M e. On ) -> ( ( ( 2nd ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) ) /\ ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc M ) -> ( 2nd ` z ) e. suc M ) )
178	177	imp 419	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 2nd ` z ) e. On /\ suc M e. On ) /\ ( ( 2nd ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) ) /\ ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc M ) ) -> ( 2nd ` z ) e. suc M )
179	174, 147, 176, 167, 178	syl22anc 1185	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 2nd ` z ) e. suc M )
180		elxp7 6338	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( suc M X. suc M ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. suc M /\ ( 2nd ` z ) e. suc M ) ) )
181	180	biimpri 198	. . . . . . . . . . . . . . . . . . 19 |- ( ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. suc M /\ ( 2nd ` z ) e. suc M ) ) -> z e. ( suc M X. suc M ) )
182	113, 170, 179, 181	syl12anc 1182	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z e. ( suc M X. suc M ) )
183	182	3expia 1155	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. ( a X. a ) ) -> ( z e. ( `' Q " { w } ) -> z e. ( suc M X. suc M ) ) )
184	183	ssrdv 3314	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) C_ ( suc M X. suc M ) )
185		ssdomg 7112	. . . . . . . . . . . . . . . 16 |- ( ( suc M X. suc M ) e. _V -> ( ( `' Q " { w } ) C_ ( suc M X. suc M ) -> ( `' Q " { w } ) ~<_ ( suc M X. suc M ) ) )
186	98, 184, 185	mpsyl 61	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) ~<_ ( suc M X. suc M ) )
187	131	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. ( a X. a ) ) -> om C_ a )
188		nnfi 7258	. . . . . . . . . . . . . . . . . . . 20 |- ( suc M e. om -> suc M e. Fin )
189		xpfi 7337	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( suc M e. Fin /\ suc M e. Fin ) -> ( suc M X. suc M ) e. Fin )
190	189	anidms 627	. . . . . . . . . . . . . . . . . . . . 21 |- ( suc M e. Fin -> ( suc M X. suc M ) e. Fin )
191		isfinite 7563	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( suc M X. suc M ) e. Fin <-> ( suc M X. suc M ) ~< om )
192	190, 191	sylib 189	. . . . . . . . . . . . . . . . . . . 20 |- ( suc M e. Fin -> ( suc M X. suc M ) ~< om )
193	188, 192	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( suc M e. om -> ( suc M X. suc M ) ~< om )
194		ssdomg 7112	. . . . . . . . . . . . . . . . . . . 20 |- ( a e. _V -> ( om C_ a -> om ~<_ a ) )
195	14, 194	ax-mp 8	. . . . . . . . . . . . . . . . . . 19 |- ( om C_ a -> om ~<_ a )
196		sdomdomtr 7199	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( suc M X. suc M ) ~< om /\ om ~<_ a ) -> ( suc M X. suc M ) ~< a )
197	193, 195, 196	syl2an 464	. . . . . . . . . . . . . . . . . 18 |- ( ( suc M e. om /\ om C_ a ) -> ( suc M X. suc M ) ~< a )
198	197	expcom 425	. . . . . . . . . . . . . . . . 17 |- ( om C_ a -> ( suc M e. om -> ( suc M X. suc M ) ~< a ) )
199	187, 198	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w e. ( a X. a ) ) -> ( suc M e. om -> ( suc M X. suc M ) ~< a ) )
200	129	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w e. ( a X. a ) ) -> A. m e. a m ~< a )
201		breq1 4175	. . . . . . . . . . . . . . . . . . 19 |- ( m = suc M -> ( m ~< a <-> suc M ~< a ) )
202	201	rspccv 3009	. . . . . . . . . . . . . . . . . 18 |- ( A. m e. a m ~< a -> ( suc M e. a -> suc M ~< a ) )
203	200, 144, 202	sylc 58	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. ( a X. a ) ) -> suc M ~< a )
204		omelon 7557	. . . . . . . . . . . . . . . . . . 19 |- om e. On
205		ontri1 4575	. . . . . . . . . . . . . . . . . . 19 |- ( ( om e. On /\ suc M e. On ) -> ( om C_ suc M <-> -. suc M e. om ) )
206	204, 146, 205	sylancr 645	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w e. ( a X. a ) ) -> ( om C_ suc M <-> -. suc M e. om ) )
207		simplr 732	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) -> A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) )
208	13, 207	sylbi 188	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) )
209	208	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ w e. ( a X. a ) ) -> A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) )
210		sseq2 3330	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = suc M -> ( om C_ m <-> om C_ suc M ) )
211		xpeq12 4856	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( m = suc M /\ m = suc M ) -> ( m X. m ) = ( suc M X. suc M ) )
212	211	anidms 627	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = suc M -> ( m X. m ) = ( suc M X. suc M ) )
213		id 20	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m = suc M -> m = suc M )
214	212, 213	breq12d 4185	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = suc M -> ( ( m X. m ) ~~ m <-> ( suc M X. suc M ) ~~ suc M ) )
215	210, 214	imbi12d 312	. . . . . . . . . . . . . . . . . . . 20 |- ( m = suc M -> ( ( om C_ m -> ( m X. m ) ~~ m ) <-> ( om C_ suc M -> ( suc M X. suc M ) ~~ suc M ) ) )
216	215	rspccv 3009	. . . . . . . . . . . . . . . . . . 19 |- ( A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) -> ( suc M e. a -> ( om C_ suc M -> ( suc M X. suc M ) ~~ suc M ) ) )
217	209, 144, 216	sylc 58	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ w e. ( a X. a ) ) -> ( om C_ suc M -> ( suc M X. suc M ) ~~ suc M ) )
218	206, 217	sylbird 227	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ w e. ( a X. a ) ) -> ( -. suc M e. om -> ( suc M X. suc M ) ~~ suc M ) )
219		ensdomtr 7202	. . . . . . . . . . . . . . . . . 18 |- ( ( ( suc M X. suc M ) ~~ suc M /\ suc M ~< a ) -> ( suc M X. suc M ) ~< a )
220	219	expcom 425	. . . . . . . . . . . . . . . . 17 |- ( suc M ~< a -> ( ( suc M X. suc M ) ~~ suc M -> ( suc M X. suc M ) ~< a ) )
221	203, 218, 220	sylsyld 54	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ w e. ( a X. a ) ) -> ( -. suc M e. om -> ( suc M X. suc M ) ~< a ) )
222	199, 221	pm2.61d 152	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ( a X. a ) ) -> ( suc M X. suc M ) ~< a )
223		domsdomtr 7201	. . . . . . . . . . . . . . 15 |- ( ( ( `' Q " { w } ) ~<_ ( suc M X. suc M ) /\ ( suc M X. suc M ) ~< a ) -> ( `' Q " { w } ) ~< a )
224	186, 222, 223	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) ~< a )
225		ensdomtr 7202	. . . . . . . . . . . . . 14 |- ( ( ( `' J ` w ) ~~ ( `' Q " { w } ) /\ ( `' Q " { w } ) ~< a ) -> ( `' J ` w ) ~< a )
226	91, 224, 225	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) ~< a )
227		ordelon 4565	. . . . . . . . . . . . . . 15 |- ( ( Ord dom J /\ ( `' J ` w ) e. dom J ) -> ( `' J ` w ) e. On )
228	78, 82, 227	sylancr 645	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) e. On )
229		onenon 7792	. . . . . . . . . . . . . . 15 |- ( a e. On -> a e. dom card )
230	114, 229	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ( a X. a ) ) -> a e. dom card )
231		cardsdomel 7817	. . . . . . . . . . . . . 14 |- ( ( ( `' J ` w ) e. On /\ a e. dom card ) -> ( ( `' J ` w ) ~< a <-> ( `' J ` w ) e. ( card ` a ) ) )
232	228, 230, 231	syl2anc 643	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. ( a X. a ) ) -> ( ( `' J ` w ) ~< a <-> ( `' J ` w ) e. ( card ` a ) ) )
233	226, 232	mpbid 202	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) e. ( card ` a ) )
234		eleq2 2465	. . . . . . . . . . . . . 14 |- ( ( card ` a ) = a -> ( ( `' J ` w ) e. ( card ` a ) <-> ( `' J ` w ) e. a ) )
235	132, 234	sylbir 205	. . . . . . . . . . . . 13 |- ( ( a e. On /\ A. m e. a m ~< a ) -> ( ( `' J ` w ) e. ( card ` a ) <-> ( `' J ` w ) e. a ) )
236	114, 200, 235	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( a X. a ) ) -> ( ( `' J ` w ) e. ( card ` a ) <-> ( `' J ` w ) e. a ) )
237	233, 236	mpbid 202	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) e. a )
238	237	ralrimiva 2749	. . . . . . . . . 10 |- ( ph -> A. w e. ( a X. a ) ( `' J ` w ) e. a )
239		fnfvrnss 5855	. . . . . . . . . . 11 |- ( ( `' J Fn ( a X. a ) /\ A. w e. ( a X. a ) ( `' J ` w ) e. a ) -> ran `' J C_ a )
240		ssdomg 7112	. . . . . . . . . . 11 |- ( a e. _V -> ( ran `' J C_ a -> ran `' J ~<_ a ) )
241	14, 239, 240	mpsyl 61	. . . . . . . . . 10 |- ( ( `' J Fn ( a X. a ) /\ A. w e. ( a X. a ) ( `' J ` w ) e. a ) -> ran `' J ~<_ a )
242	46, 238, 241	syl2anc 643	. . . . . . . . 9 |- ( ph -> ran `' J ~<_ a )
243		endomtr 7124	. . . . . . . . 9 |- ( ( ( a X. a ) ~~ ran `' J /\ ran `' J ~<_ a ) -> ( a X. a ) ~<_ a )
244	44, 242, 243	syl2anc 643	. . . . . . . 8 |- ( ph -> ( a X. a ) ~<_ a )
245	13, 244	sylbir 205	. . . . . . 7 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) -> ( a X. a ) ~<_ a )
246		df1o2 6695	. . . . . . . . . . . 12 |- 1o = { (/) }
247		1onn 6841	. . . . . . . . . . . 12 |- 1o e. om
248	246, 247	eqeltrri 2475	. . . . . . . . . . 11 |- { (/) } e. om
249		nnsdom 7564	. . . . . . . . . . 11 |- ( { (/) } e. om -> { (/) } ~< om )
250		sdomdom 7094	. . . . . . . . . . 11 |- ( { (/) } ~< om -> { (/) } ~<_ om )
251	248, 249, 250	mp2b 10	. . . . . . . . . 10 |- { (/) } ~<_ om
252		domtr 7119	. . . . . . . . . 10 |- ( ( { (/) } ~<_ om /\ om ~<_ a ) -> { (/) } ~<_ a )
253	251, 195, 252	sylancr 645	. . . . . . . . 9 |- ( om C_ a -> { (/) } ~<_ a )
254		0ex 4299	. . . . . . . . . . . 12 |- (/) e. _V
255	14, 254	xpsnen 7151	. . . . . . . . . . 11 |- ( a X. { (/) } ) ~~ a
256	255	ensymi 7116	. . . . . . . . . 10 |- a ~~ ( a X. { (/) } )
257	14	xpdom2 7162	. . . . . . . . . 10 |- ( { (/) } ~<_ a -> ( a X. { (/) } ) ~<_ ( a X. a ) )
258		endomtr 7124	. . . . . . . . . 10 |- ( ( a ~~ ( a X. { (/) } ) /\ ( a X. { (/) } ) ~<_ ( a X. a ) ) -> a ~<_ ( a X. a ) )
259	256, 257, 258	sylancr 645	. . . . . . . . 9 |- ( { (/) } ~<_ a -> a ~<_ ( a X. a ) )
260	253, 259	syl 16	. . . . . . . 8 |- ( om C_ a -> a ~<_ ( a X. a ) )
261	260	ad2antrl 709	. . . . . . 7 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) -> a ~<_ ( a X. a ) )
262		sbth 7186	. . . . . . 7 |- ( ( ( a X. a ) ~<_ a /\ a ~<_ ( a X. a ) ) -> ( a X. a ) ~~ a )
263	245, 261, 262	syl2anc 643	. . . . . 6 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ A. m e. a m ~< a ) ) -> ( a X. a ) ~~ a )
264	263	expr 599	. . . . 5 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ om C_ a ) -> ( A. m e. a m ~< a -> ( a X. a ) ~~ a ) )
265		simplr 732	. . . . . . . 8 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ -. A. m e. a m ~< a ) ) -> A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) )
266		simpll 731	. . . . . . . . 9 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ -. A. m e. a m ~< a ) ) -> a e. On )
267		simprr 734	. . . . . . . . 9 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ -. A. m e. a m ~< a ) ) -> -. A. m e. a m ~< a )
268		rexnal 2677	. . . . . . . . . 10 |- ( E. m e. a -. m ~< a <-> -. A. m e. a m ~< a )
269		onelss 4583	. . . . . . . . . . . . 13 |- ( a e. On -> ( m e. a -> m C_ a ) )
270		ssdomg 7112	. . . . . . . . . . . . 13 |- ( a e. On -> ( m C_ a -> m ~<_ a ) )
271	269, 270	syld 42	. . . . . . . . . . . 12 |- ( a e. On -> ( m e. a -> m ~<_ a ) )
272		bren2 7097	. . . . . . . . . . . . 13 |- ( m ~~ a <-> ( m ~<_ a /\ -. m ~< a ) )
273	272	simplbi2 609	. . . . . . . . . . . 12 |- ( m ~<_ a -> ( -. m ~< a -> m ~~ a ) )
274	271, 273	syl6 31	. . . . . . . . . . 11 |- ( a e. On -> ( m e. a -> ( -. m ~< a -> m ~~ a ) ) )
275	274	reximdvai 2776	. . . . . . . . . 10 |- ( a e. On -> ( E. m e. a -. m ~< a -> E. m e. a m ~~ a ) )
276	268, 275	syl5bir 210	. . . . . . . . 9 |- ( a e. On -> ( -. A. m e. a m ~< a -> E. m e. a m ~~ a ) )
277	266, 267, 276	sylc 58	. . . . . . . 8 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ -. A. m e. a m ~< a ) ) -> E. m e. a m ~~ a )
278		r19.29 2806	. . . . . . . 8 |- ( ( A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) /\ E. m e. a m ~~ a ) -> E. m e. a ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) )
279	265, 277, 278	syl2anc 643	. . . . . . 7 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ -. A. m e. a m ~< a ) ) -> E. m e. a ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) )
280		simprl 733	. . . . . . . 8 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ -. A. m e. a m ~< a ) ) -> om C_ a )
281		onelon 4566	. . . . . . . . . . . . . . . . 17 |- ( ( a e. On /\ m e. a ) -> m e. On )
282		ensym 7115	. . . . . . . . . . . . . . . . . 18 |- ( m ~~ a -> a ~~ m )
283		domentr 7125	. . . . . . . . . . . . . . . . . 18 |- ( ( om ~<_ a /\ a ~~ m ) -> om ~<_ m )
284	195, 282, 283	syl2an 464	. . . . . . . . . . . . . . . . 17 |- ( ( om C_ a /\ m ~~ a ) -> om ~<_ m )
285		domnsym 7192	. . . . . . . . . . . . . . . . . . 19 |- ( om ~<_ m -> -. m ~< om )
286		nnsdom 7564	. . . . . . . . . . . . . . . . . . 19 |- ( m e. om -> m ~< om )
287	285, 286	nsyl 115	. . . . . . . . . . . . . . . . . 18 |- ( om ~<_ m -> -. m e. om )
288		ontri1 4575	. . . . . . . . . . . . . . . . . . 19 |- ( ( om e. On /\ m e. On ) -> ( om C_ m <-> -. m e. om ) )
289	204, 288	mpan 652	. . . . . . . . . . . . . . . . . 18 |- ( m e. On -> ( om C_ m <-> -. m e. om ) )
290	287, 289	syl5ibr 213	. . . . . . . . . . . . . . . . 17 |- ( m e. On -> ( om ~<_ m -> om C_ m ) )
291	281, 284, 290	syl2im 36	. . . . . . . . . . . . . . . 16 |- ( ( a e. On /\ m e. a ) -> ( ( om C_ a /\ m ~~ a ) -> om C_ m ) )
292	291	exp3a 426	. . . . . . . . . . . . . . 15 |- ( ( a e. On /\ m e. a ) -> ( om C_ a -> ( m ~~ a -> om C_ m ) ) )
293	292	impcom 420	. . . . . . . . . . . . . 14 |- ( ( om C_ a /\ ( a e. On /\ m e. a ) ) -> ( m ~~ a -> om C_ m ) )
294	293	imim1d 71	. . . . . . . . . . . . 13 |- ( ( om C_ a /\ ( a e. On /\ m e. a ) ) -> ( ( om C_ m -> ( m X. m ) ~~ m ) -> ( m ~~ a -> ( m X. m ) ~~ m ) ) )
295	294	imp32 423	. . . . . . . . . . . 12 |- ( ( ( om C_ a /\ ( a e. On /\ m e. a ) ) /\ ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) ) -> ( m X. m ) ~~ m )
296		entr 7118	. . . . . . . . . . . . . . . 16 |- ( ( ( m X. m ) ~~ m /\ m ~~ a ) -> ( m X. m ) ~~ a )
297	296	ancoms 440	. . . . . . . . . . . . . . 15 |- ( ( m ~~ a /\ ( m X. m ) ~~ m ) -> ( m X. m ) ~~ a )
298		xpen 7229	. . . . . . . . . . . . . . . . . 18 |- ( ( a ~~ m /\ a ~~ m ) -> ( a X. a ) ~~ ( m X. m ) )
299	298	anidms 627	. . . . . . . . . . . . . . . . 17 |- ( a ~~ m -> ( a X. a ) ~~ ( m X. m ) )
300		entr 7118	. . . . . . . . . . . . . . . . 17 |- ( ( ( a X. a ) ~~ ( m X. m ) /\ ( m X. m ) ~~ a ) -> ( a X. a ) ~~ a )
301	299, 300	sylan 458	. . . . . . . . . . . . . . . 16 |- ( ( a ~~ m /\ ( m X. m ) ~~ a ) -> ( a X. a ) ~~ a )
302	282, 301	sylan 458	. . . . . . . . . . . . . . 15 |- ( ( m ~~ a /\ ( m X. m ) ~~ a ) -> ( a X. a ) ~~ a )
303	297, 302	syldan 457	. . . . . . . . . . . . . 14 |- ( ( m ~~ a /\ ( m X. m ) ~~ m ) -> ( a X. a ) ~~ a )
304	303	ex 424	. . . . . . . . . . . . 13 |- ( m ~~ a -> ( ( m X. m ) ~~ m -> ( a X. a ) ~~ a ) )
305	304	ad2antll 710	. . . . . . . . . . . 12 |- ( ( ( om C_ a /\ ( a e. On /\ m e. a ) ) /\ ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) ) -> ( ( m X. m ) ~~ m -> ( a X. a ) ~~ a ) )
306	295, 305	mpd 15	. . . . . . . . . . 11 |- ( ( ( om C_ a /\ ( a e. On /\ m e. a ) ) /\ ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) ) -> ( a X. a ) ~~ a )
307	306	ex 424	. . . . . . . . . 10 |- ( ( om C_ a /\ ( a e. On /\ m e. a ) ) -> ( ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) -> ( a X. a ) ~~ a ) )
308	307	expr 599	. . . . . . . . 9 |- ( ( om C_ a /\ a e. On ) -> ( m e. a -> ( ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) -> ( a X. a ) ~~ a ) ) )
309	308	rexlimdv 2789	. . . . . . . 8 |- ( ( om C_ a /\ a e. On ) -> ( E. m e. a ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) -> ( a X. a ) ~~ a ) )
310	280, 266, 309	syl2anc 643	. . . . . . 7 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ -. A. m e. a m ~< a ) ) -> ( E. m e. a ( ( om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) -> ( a X. a ) ~~ a ) )
311	279, 310	mpd 15	. . . . . 6 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ ( om C_ a /\ -. A. m e. a m ~< a ) ) -> ( a X. a ) ~~ a )
312	311	expr 599	. . . . 5 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ om C_ a ) -> ( -. A. m e. a m ~< a -> ( a X. a ) ~~ a ) )
313	264, 312	pm2.61d 152	. . . 4 |- ( ( ( a e. On /\ A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) ) /\ om C_ a ) -> ( a X. a ) ~~ a )
314	313	exp31 588	. . 3 |- ( a e. On -> ( A. m e. a ( om C_ m -> ( m X. m ) ~~ m ) -> ( om C_ a -> ( a X. a ) ~~ a ) ) )
315	6, 12, 314	tfis3 4796	. 2 |- ( A e. On -> ( om C_ A -> ( A X. A ) ~~ A ) )
316	315	imp 419	1 |- ( ( A e. On /\ om C_ A ) -> ( A X. A ) ~~ A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2666   E.wrex 2667   _Vcvv 2916   u. cun 3278   i^i cin 3279   C_ wss 3280   (/)c0 3588   {csn 3774   <.cop 3777   class class class wbr 4172   {copab 4225   _E cep 4452   Se wse 4499   We wwe 4500   Ord word 4540   Oncon0 4541   Lim wlim 4542   suc csuc 4543   omcom 4804   X. cxp 4835   `'ccnv 4836   dom cdm 4837   ran crn 4838   |` cres 4839   "cima 4840   Fn wfn 5408   -->wf 5409   -1-1->wf1 5410   -1-1-onto->wf1o 5412   ` cfv 5413   Isom wiso 5414   1stc1st 6306   2ndc2nd 6307   1oc1o 6676   ~~ cen 7065   ~<_ cdom 7066   ~< csdm 7067   Fincfn 7068  OrdIsocoi 7434   cardccrd 7778

This theorem is referenced by:  infxpen  7852

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-card 7782