Metamath Proof Explorer

Theorem infxpenlem

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

Ref Expression
Hypotheses 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 infxpenlem 
|- ( ( A e. On /\ _om C_ A ) -> ( A X. A ) ~~ A )

Proof

Step Hyp Ref Expression
1 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 ) ) ) ) }
2 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 ) ) ) }
3 infxpen.1 
 |-  Q = ( R i^i ( ( a X. a ) X. ( a X. a ) ) )
4 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 ) ) )
5 infxpen.3 
 |-  M = ( ( 1st ` w ) u. ( 2nd ` w ) )
6 infxpen.4 
 |-  J = OrdIso ( Q , ( a X. a ) )
7 sseq2 
 |-  ( a = m -> ( _om C_ a <-> _om C_ m ) )
8 xpeq12 
 |-  ( ( a = m /\ a = m ) -> ( a X. a ) = ( m X. m ) )
9 8 anidms 
 |-  ( a = m -> ( a X. a ) = ( m X. m ) )
10 id 
 |-  ( a = m -> a = m )
11 9 10 breq12d 
 |-  ( a = m -> ( ( a X. a ) ~~ a <-> ( m X. m ) ~~ m ) )
12 7 11 imbi12d 
 |-  ( a = m -> ( ( _om C_ a -> ( a X. a ) ~~ a ) <-> ( _om C_ m -> ( m X. m ) ~~ m ) ) )
13 sseq2 
 |-  ( a = A -> ( _om C_ a <-> _om C_ A ) )
14 xpeq12 
 |-  ( ( a = A /\ a = A ) -> ( a X. a ) = ( A X. A ) )
15 14 anidms 
 |-  ( a = A -> ( a X. a ) = ( A X. A ) )
16 id 
 |-  ( a = A -> a = A )
17 15 16 breq12d 
 |-  ( a = A -> ( ( a X. a ) ~~ a <-> ( A X. A ) ~~ A ) )
18 13 17 imbi12d 
 |-  ( a = A -> ( ( _om C_ a -> ( a X. a ) ~~ a ) <-> ( _om C_ A -> ( A X. A ) ~~ A ) ) )
19 vex 
 |-  a e. _V
20 19 19 xpex 
 |-  ( a X. a ) e. _V
21 simpll 
 |-  ( ( ( 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 )
22 4 21 sylbi 
 |-  ( ph -> a e. On )
23 onss 
 |-  ( a e. On -> a C_ On )
24 22 23 syl 
 |-  ( ph -> a C_ On )
25 xpss12 
 |-  ( ( a C_ On /\ a C_ On ) -> ( a X. a ) C_ ( On X. On ) )
26 24 24 25 syl2anc 
 |-  ( ph -> ( a X. a ) C_ ( On X. On ) )
27 1 2 r0weon 
 |-  ( R We ( On X. On ) /\ R Se ( On X. On ) )
28 27 simpli 
 |-  R We ( On X. On )
29 wess 
 |-  ( ( a X. a ) C_ ( On X. On ) -> ( R We ( On X. On ) -> R We ( a X. a ) ) )
30 26 28 29 mpisyl 
 |-  ( ph -> R We ( a X. a ) )
31 weinxp 
 |-  ( R We ( a X. a ) <-> ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) We ( a X. a ) )
32 30 31 sylib 
 |-  ( ph -> ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) We ( a X. a ) )
33 weeq1 
 |-  ( 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 ) ) )
34 3 33 ax-mp 
 |-  ( Q We ( a X. a ) <-> ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) We ( a X. a ) )
35 32 34 sylibr 
 |-  ( ph -> Q We ( a X. a ) )
36 6 oiiso 
 |-  ( ( ( a X. a ) e. _V /\ Q We ( a X. a ) ) -> J Isom _E , Q ( dom J , ( a X. a ) ) )
37 20 35 36 sylancr 
 |-  ( ph -> J Isom _E , Q ( dom J , ( a X. a ) ) )
38 isof1o 
 |-  ( J Isom _E , Q ( dom J , ( a X. a ) ) -> J : dom J -1-1-onto-> ( a X. a ) )
39 f1ocnv 
 |-  ( J : dom J -1-1-onto-> ( a X. a ) -> `' J : ( a X. a ) -1-1-onto-> dom J )
40 f1of1 
 |-  ( `' J : ( a X. a ) -1-1-onto-> dom J -> `' J : ( a X. a ) -1-1-> dom J )
41 37 38 39 40 4syl 
 |-  ( ph -> `' J : ( a X. a ) -1-1-> dom J )
42 f1f1orn 
 |-  ( `' J : ( a X. a ) -1-1-> dom J -> `' J : ( a X. a ) -1-1-onto-> ran `' J )
43 20 f1oen 
 |-  ( `' J : ( a X. a ) -1-1-onto-> ran `' J -> ( a X. a ) ~~ ran `' J )
44 41 42 43 3syl 
 |-  ( ph -> ( a X. a ) ~~ ran `' J )
45 f1ofn 
 |-  ( `' J : ( a X. a ) -1-1-onto-> dom J -> `' J Fn ( a X. a ) )
46 37 38 39 45 4syl 
 |-  ( ph -> `' J Fn ( a X. a ) )
47 37 adantr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> J Isom _E , Q ( dom J , ( a X. a ) ) )
48 38 39 40 3syl 
 |-  ( J Isom _E , Q ( dom J , ( a X. a ) ) -> `' J : ( a X. a ) -1-1-> dom J )
49 cnvimass 
 |-  ( `' Q " { w } ) C_ dom Q
50 inss2 
 |-  ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) C_ ( ( a X. a ) X. ( a X. a ) )
51 3 50 eqsstri 
 |-  Q C_ ( ( a X. a ) X. ( a X. a ) )
52 dmss 
 |-  ( 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 
 |-  dom Q C_ dom ( ( a X. a ) X. ( a X. a ) )
54 dmxpid 
 |-  dom ( ( a X. a ) X. ( a X. a ) ) = ( a X. a )
55 53 54 sseqtri 
 |-  dom Q C_ ( a X. a )
56 49 55 sstri 
 |-  ( `' Q " { w } ) C_ ( a X. a )
57 f1ores 
 |-  ( ( `' 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 
 |-  ( J Isom _E , Q ( dom J , ( a X. a ) ) -> ( `' J |` ( `' Q " { w } ) ) : ( `' Q " { w } ) -1-1-onto-> ( `' J " ( `' Q " { w } ) ) )
59 20 20 xpex 
 |-  ( ( a X. a ) X. ( a X. a ) ) e. _V
60 59 inex2 
 |-  ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) e. _V
61 3 60 eqeltri 
 |-  Q e. _V
62 61 cnvex 
 |-  `' Q e. _V
63 62 imaex 
 |-  ( `' Q " { w } ) e. _V
64 63 f1oen 
 |-  ( ( `' J |` ( `' Q " { w } ) ) : ( `' Q " { w } ) -1-1-onto-> ( `' J " ( `' Q " { w } ) ) -> ( `' Q " { w } ) ~~ ( `' J " ( `' Q " { w } ) ) )
65 47 58 64 3syl 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) ~~ ( `' J " ( `' Q " { w } ) ) )
66 sseqin2 
 |-  ( ( `' Q " { w } ) C_ ( a X. a ) <-> ( ( a X. a ) i^i ( `' Q " { w } ) ) = ( `' Q " { w } ) )
67 56 66 mpbi 
 |-  ( ( a X. a ) i^i ( `' Q " { w } ) ) = ( `' Q " { w } )
68 67 imaeq2i 
 |-  ( `' J " ( ( a X. a ) i^i ( `' Q " { w } ) ) ) = ( `' J " ( `' Q " { w } ) )
69 isocnv 
 |-  ( J Isom _E , Q ( dom J , ( a X. a ) ) -> `' J Isom Q , _E ( ( a X. a ) , dom J ) )
70 47 69 syl 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> `' J Isom Q , _E ( ( a X. a ) , dom J ) )
71 simpr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> w e. ( a X. a ) )
72 isoini 
 |-  ( ( `' 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 ) } ) ) )
73 70 71 72 syl2anc 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J " ( ( a X. a ) i^i ( `' Q " { w } ) ) ) = ( dom J i^i ( `' _E " { ( `' J ` w ) } ) ) )
74 fvex 
 |-  ( `' J ` w ) e. _V
75 74 epini 
 |-  ( `' _E " { ( `' J ` w ) } ) = ( `' J ` w )
76 75 ineq2i 
 |-  ( dom J i^i ( `' _E " { ( `' J ` w ) } ) ) = ( dom J i^i ( `' J ` w ) )
77 6 oicl 
 |-  Ord dom J
78 f1of 
 |-  ( `' J : ( a X. a ) -1-1-onto-> dom J -> `' J : ( a X. a ) --> dom J )
79 37 38 39 78 4syl 
 |-  ( ph -> `' J : ( a X. a ) --> dom J )
80 79 ffvelrnda 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) e. dom J )
81 ordelss 
 |-  ( ( Ord dom J /\ ( `' J ` w ) e. dom J ) -> ( `' J ` w ) C_ dom J )
82 77 80 81 sylancr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) C_ dom J )
83 sseqin2 
 |-  ( ( `' J ` w ) C_ dom J <-> ( dom J i^i ( `' J ` w ) ) = ( `' J ` w ) )
84 82 83 sylib 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( dom J i^i ( `' J ` w ) ) = ( `' J ` w ) )
85 76 84 syl5eq 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( dom J i^i ( `' _E " { ( `' J ` w ) } ) ) = ( `' J ` w ) )
86 73 85 eqtrd 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J " ( ( a X. a ) i^i ( `' Q " { w } ) ) ) = ( `' J ` w ) )
87 68 86 eqtr3id 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J " ( `' Q " { w } ) ) = ( `' J ` w ) )
88 65 87 breqtrd 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) ~~ ( `' J ` w ) )
89 88 ensymd 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) ~~ ( `' Q " { w } ) )
90 fvex 
 |-  ( 1st ` w ) e. _V
91 fvex 
 |-  ( 2nd ` w ) e. _V
92 90 91 unex 
 |-  ( ( 1st ` w ) u. ( 2nd ` w ) ) e. _V
93 5 92 eqeltri 
 |-  M e. _V
94 93 sucex 
 |-  suc M e. _V
95 94 94 xpex 
 |-  ( suc M X. suc M ) e. _V
96 xpss 
 |-  ( a X. a ) C_ ( _V X. _V )
97 simp3 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z e. ( `' Q " { w } ) )
98 vex 
 |-  z e. _V
99 98 eliniseg 
 |-  ( w e. _V -> ( z e. ( `' Q " { w } ) <-> z Q w ) )
100 99 elv 
 |-  ( z e. ( `' Q " { w } ) <-> z Q w )
101 97 100 sylib 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z Q w )
102 3 breqi 
 |-  ( z Q w <-> z ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) w )
103 brin 
 |-  ( z ( R i^i ( ( a X. a ) X. ( a X. a ) ) ) w <-> ( z R w /\ z ( ( a X. a ) X. ( a X. a ) ) w ) )
104 102 103 bitri 
 |-  ( z Q w <-> ( z R w /\ z ( ( a X. a ) X. ( a X. a ) ) w ) )
105 104 simprbi 
 |-  ( z Q w -> z ( ( a X. a ) X. ( a X. a ) ) w )
106 brxp 
 |-  ( z ( ( a X. a ) X. ( a X. a ) ) w <-> ( z e. ( a X. a ) /\ w e. ( a X. a ) ) )
107 106 simplbi 
 |-  ( z ( ( a X. a ) X. ( a X. a ) ) w -> z e. ( a X. a ) )
108 101 105 107 3syl 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z e. ( a X. a ) )
109 96 108 sseldi 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z e. ( _V X. _V ) )
110 22 adantr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> a e. On )
111 110 3adant3 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> a e. On )
112 xp1st 
 |-  ( z e. ( a X. a ) -> ( 1st ` z ) e. a )
113 onelon 
 |-  ( ( a e. On /\ ( 1st ` z ) e. a ) -> ( 1st ` z ) e. On )
114 112 113 sylan2 
 |-  ( ( a e. On /\ z e. ( a X. a ) ) -> ( 1st ` z ) e. On )
115 111 108 114 syl2anc 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 1st ` z ) e. On )
116 eloni 
 |-  ( a e. On -> Ord a )
117 elxp7 
 |-  ( w e. ( a X. a ) <-> ( w e. ( _V X. _V ) /\ ( ( 1st ` w ) e. a /\ ( 2nd ` w ) e. a ) ) )
118 117 simprbi 
 |-  ( w e. ( a X. a ) -> ( ( 1st ` w ) e. a /\ ( 2nd ` w ) e. a ) )
119 ordunel 
 |-  ( ( Ord a /\ ( 1st ` w ) e. a /\ ( 2nd ` w ) e. a ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. a )
120 119 3expib 
 |-  ( Ord a -> ( ( ( 1st ` w ) e. a /\ ( 2nd ` w ) e. a ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. a ) )
121 116 118 120 syl2im 
 |-  ( a e. On -> ( w e. ( a X. a ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. a ) )
122 110 71 121 sylc 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. a )
123 5 122 eqeltrid 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> M e. a )
124 simprr 
 |-  ( ( ( 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 )
125 4 124 sylbi 
 |-  ( ph -> A. m e. a m ~< a )
126 simprl 
 |-  ( ( ( 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 )
127 4 126 sylbi 
 |-  ( ph -> _om C_ a )
128 iscard 
 |-  ( ( card ` a ) = a <-> ( a e. On /\ A. m e. a m ~< a ) )
129 cardlim 
 |-  ( _om C_ ( card ` a ) <-> Lim ( card ` a ) )
130 sseq2 
 |-  ( ( card ` a ) = a -> ( _om C_ ( card ` a ) <-> _om C_ a ) )
131 limeq 
 |-  ( ( card ` a ) = a -> ( Lim ( card ` a ) <-> Lim a ) )
132 130 131 bibi12d 
 |-  ( ( card ` a ) = a -> ( ( _om C_ ( card ` a ) <-> Lim ( card ` a ) ) <-> ( _om C_ a <-> Lim a ) ) )
133 129 132 mpbii 
 |-  ( ( card ` a ) = a -> ( _om C_ a <-> Lim a ) )
134 128 133 sylbir 
 |-  ( ( a e. On /\ A. m e. a m ~< a ) -> ( _om C_ a <-> Lim a ) )
135 134 biimpa 
 |-  ( ( ( a e. On /\ A. m e. a m ~< a ) /\ _om C_ a ) -> Lim a )
136 22 125 127 135 syl21anc 
 |-  ( ph -> Lim a )
137 136 adantr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> Lim a )
138 limsuc 
 |-  ( Lim a -> ( M e. a <-> suc M e. a ) )
139 137 138 syl 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( M e. a <-> suc M e. a ) )
140 123 139 mpbid 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> suc M e. a )
141 onelon 
 |-  ( ( a e. On /\ suc M e. a ) -> suc M e. On )
142 22 140 141 syl2an2r 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> suc M e. On )
143 142 3adant3 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> suc M e. On )
144 ssun1 
 |-  ( 1st ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) )
145 144 a1i 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 1st ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) ) )
146 104 simplbi 
 |-  ( z Q w -> z R w )
147 df-br 
 |-  ( z R w <-> <. z , w >. e. R )
148 2 eleq2i 
 |-  ( <. 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 ) ) ) } )
149 opabidw 
 |-  ( <. 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 ) ) ) )
150 147 148 149 3bitri 
 |-  ( 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 ) ) ) )
151 150 simprbi 
 |-  ( 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 ) ) )
152 simpl 
 |-  ( ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z L w ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) )
153 152 orim2i 
 |-  ( ( ( ( 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 ) ) ) )
154 151 153 syl 
 |-  ( z R w -> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )
155 fvex 
 |-  ( 1st ` z ) e. _V
156 fvex 
 |-  ( 2nd ` z ) e. _V
157 155 156 unex 
 |-  ( ( 1st ` z ) u. ( 2nd ` z ) ) e. _V
158 157 elsuc 
 |-  ( ( ( 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 ) ) ) )
159 154 158 sylibr 
 |-  ( z R w -> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc ( ( 1st ` w ) u. ( 2nd ` w ) ) )
160 suceq 
 |-  ( M = ( ( 1st ` w ) u. ( 2nd ` w ) ) -> suc M = suc ( ( 1st ` w ) u. ( 2nd ` w ) ) )
161 5 160 ax-mp 
 |-  suc M = suc ( ( 1st ` w ) u. ( 2nd ` w ) )
162 159 161 eleqtrrdi 
 |-  ( z R w -> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc M )
163 101 146 162 3syl 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. suc M )
164 ontr2 
 |-  ( ( ( 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 ) )
165 164 imp 
 |-  ( ( ( ( 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 )
166 115 143 145 163 165 syl22anc 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 1st ` z ) e. suc M )
167 xp2nd 
 |-  ( z e. ( a X. a ) -> ( 2nd ` z ) e. a )
168 onelon 
 |-  ( ( a e. On /\ ( 2nd ` z ) e. a ) -> ( 2nd ` z ) e. On )
169 167 168 sylan2 
 |-  ( ( a e. On /\ z e. ( a X. a ) ) -> ( 2nd ` z ) e. On )
170 111 108 169 syl2anc 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 2nd ` z ) e. On )
171 ssun2 
 |-  ( 2nd ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) )
172 171 a1i 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 2nd ` z ) C_ ( ( 1st ` z ) u. ( 2nd ` z ) ) )
173 ontr2 
 |-  ( ( ( 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 ) )
174 173 imp 
 |-  ( ( ( ( 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 )
175 170 143 172 163 174 syl22anc 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> ( 2nd ` z ) e. suc M )
176 elxp7 
 |-  ( z e. ( suc M X. suc M ) <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. suc M /\ ( 2nd ` z ) e. suc M ) ) )
177 176 biimpri 
 |-  ( ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) e. suc M /\ ( 2nd ` z ) e. suc M ) ) -> z e. ( suc M X. suc M ) )
178 109 166 175 177 syl12anc 
 |-  ( ( ph /\ w e. ( a X. a ) /\ z e. ( `' Q " { w } ) ) -> z e. ( suc M X. suc M ) )
179 178 3expia 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( z e. ( `' Q " { w } ) -> z e. ( suc M X. suc M ) ) )
180 179 ssrdv 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) C_ ( suc M X. suc M ) )
181 ssdomg 
 |-  ( ( suc M X. suc M ) e. _V -> ( ( `' Q " { w } ) C_ ( suc M X. suc M ) -> ( `' Q " { w } ) ~<_ ( suc M X. suc M ) ) )
182 95 180 181 mpsyl 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) ~<_ ( suc M X. suc M ) )
183 127 adantr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> _om C_ a )
184 nnfi 
 |-  ( suc M e. _om -> suc M e. Fin )
185 xpfi 
 |-  ( ( suc M e. Fin /\ suc M e. Fin ) -> ( suc M X. suc M ) e. Fin )
186 185 anidms 
 |-  ( suc M e. Fin -> ( suc M X. suc M ) e. Fin )
187 isfinite 
 |-  ( ( suc M X. suc M ) e. Fin <-> ( suc M X. suc M ) ~< _om )
188 186 187 sylib 
 |-  ( suc M e. Fin -> ( suc M X. suc M ) ~< _om )
189 184 188 syl 
 |-  ( suc M e. _om -> ( suc M X. suc M ) ~< _om )
190 ssdomg 
 |-  ( a e. _V -> ( _om C_ a -> _om ~<_ a ) )
191 190 elv 
 |-  ( _om C_ a -> _om ~<_ a )
192 sdomdomtr 
 |-  ( ( ( suc M X. suc M ) ~< _om /\ _om ~<_ a ) -> ( suc M X. suc M ) ~< a )
193 189 191 192 syl2an 
 |-  ( ( suc M e. _om /\ _om C_ a ) -> ( suc M X. suc M ) ~< a )
194 193 expcom 
 |-  ( _om C_ a -> ( suc M e. _om -> ( suc M X. suc M ) ~< a ) )
195 183 194 syl 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( suc M e. _om -> ( suc M X. suc M ) ~< a ) )
196 breq1 
 |-  ( m = suc M -> ( m ~< a <-> suc M ~< a ) )
197 125 adantr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> A. m e. a m ~< a )
198 196 197 140 rspcdva 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> suc M ~< a )
199 omelon 
 |-  _om e. On
200 ontri1 
 |-  ( ( _om e. On /\ suc M e. On ) -> ( _om C_ suc M <-> -. suc M e. _om ) )
201 199 142 200 sylancr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( _om C_ suc M <-> -. suc M e. _om ) )
202 sseq2 
 |-  ( m = suc M -> ( _om C_ m <-> _om C_ suc M ) )
203 xpeq12 
 |-  ( ( m = suc M /\ m = suc M ) -> ( m X. m ) = ( suc M X. suc M ) )
204 203 anidms 
 |-  ( m = suc M -> ( m X. m ) = ( suc M X. suc M ) )
205 id 
 |-  ( m = suc M -> m = suc M )
206 204 205 breq12d 
 |-  ( m = suc M -> ( ( m X. m ) ~~ m <-> ( suc M X. suc M ) ~~ suc M ) )
207 202 206 imbi12d 
 |-  ( m = suc M -> ( ( _om C_ m -> ( m X. m ) ~~ m ) <-> ( _om C_ suc M -> ( suc M X. suc M ) ~~ suc M ) ) )
208 simplr 
 |-  ( ( ( 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 ) )
209 4 208 sylbi 
 |-  ( ph -> A. m e. a ( _om C_ m -> ( m X. m ) ~~ m ) )
210 209 adantr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> A. m e. a ( _om C_ m -> ( m X. m ) ~~ m ) )
211 207 210 140 rspcdva 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( _om C_ suc M -> ( suc M X. suc M ) ~~ suc M ) )
212 201 211 sylbird 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( -. suc M e. _om -> ( suc M X. suc M ) ~~ suc M ) )
213 ensdomtr 
 |-  ( ( ( suc M X. suc M ) ~~ suc M /\ suc M ~< a ) -> ( suc M X. suc M ) ~< a )
214 213 expcom 
 |-  ( suc M ~< a -> ( ( suc M X. suc M ) ~~ suc M -> ( suc M X. suc M ) ~< a ) )
215 198 212 214 sylsyld 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( -. suc M e. _om -> ( suc M X. suc M ) ~< a ) )
216 195 215 pm2.61d 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( suc M X. suc M ) ~< a )
217 domsdomtr 
 |-  ( ( ( `' Q " { w } ) ~<_ ( suc M X. suc M ) /\ ( suc M X. suc M ) ~< a ) -> ( `' Q " { w } ) ~< a )
218 182 216 217 syl2anc 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' Q " { w } ) ~< a )
219 ensdomtr 
 |-  ( ( ( `' J ` w ) ~~ ( `' Q " { w } ) /\ ( `' Q " { w } ) ~< a ) -> ( `' J ` w ) ~< a )
220 89 218 219 syl2anc 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) ~< a )
221 ordelon 
 |-  ( ( Ord dom J /\ ( `' J ` w ) e. dom J ) -> ( `' J ` w ) e. On )
222 77 80 221 sylancr 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) e. On )
223 onenon 
 |-  ( a e. On -> a e. dom card )
224 110 223 syl 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> a e. dom card )
225 cardsdomel 
 |-  ( ( ( `' J ` w ) e. On /\ a e. dom card ) -> ( ( `' J ` w ) ~< a <-> ( `' J ` w ) e. ( card ` a ) ) )
226 222 224 225 syl2anc 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( ( `' J ` w ) ~< a <-> ( `' J ` w ) e. ( card ` a ) ) )
227 220 226 mpbid 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) e. ( card ` a ) )
228 eleq2 
 |-  ( ( card ` a ) = a -> ( ( `' J ` w ) e. ( card ` a ) <-> ( `' J ` w ) e. a ) )
229 128 228 sylbir 
 |-  ( ( a e. On /\ A. m e. a m ~< a ) -> ( ( `' J ` w ) e. ( card ` a ) <-> ( `' J ` w ) e. a ) )
230 22 197 229 syl2an2r 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( ( `' J ` w ) e. ( card ` a ) <-> ( `' J ` w ) e. a ) )
231 227 230 mpbid 
 |-  ( ( ph /\ w e. ( a X. a ) ) -> ( `' J ` w ) e. a )
232 231 ralrimiva 
 |-  ( ph -> A. w e. ( a X. a ) ( `' J ` w ) e. a )
233 fnfvrnss 
 |-  ( ( `' J Fn ( a X. a ) /\ A. w e. ( a X. a ) ( `' J ` w ) e. a ) -> ran `' J C_ a )
234 ssdomg 
 |-  ( a e. _V -> ( ran `' J C_ a -> ran `' J ~<_ a ) )
235 19 233 234 mpsyl 
 |-  ( ( `' J Fn ( a X. a ) /\ A. w e. ( a X. a ) ( `' J ` w ) e. a ) -> ran `' J ~<_ a )
236 46 232 235 syl2anc 
 |-  ( ph -> ran `' J ~<_ a )
237 endomtr 
 |-  ( ( ( a X. a ) ~~ ran `' J /\ ran `' J ~<_ a ) -> ( a X. a ) ~<_ a )
238 44 236 237 syl2anc 
 |-  ( ph -> ( a X. a ) ~<_ a )
239 4 238 sylbir 
 |-  ( ( ( 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 )
240 df1o2 
 |-  1o = { (/) }
241 1onn 
 |-  1o e. _om
242 240 241 eqeltrri 
 |-  { (/) } e. _om
243 nnsdom 
 |-  ( { (/) } e. _om -> { (/) } ~< _om )
244 sdomdom 
 |-  ( { (/) } ~< _om -> { (/) } ~<_ _om )
245 242 243 244 mp2b 
 |-  { (/) } ~<_ _om
246 domtr 
 |-  ( ( { (/) } ~<_ _om /\ _om ~<_ a ) -> { (/) } ~<_ a )
247 245 191 246 sylancr 
 |-  ( _om C_ a -> { (/) } ~<_ a )
248 0ex 
 |-  (/) e. _V
249 19 248 xpsnen 
 |-  ( a X. { (/) } ) ~~ a
250 249 ensymi 
 |-  a ~~ ( a X. { (/) } )
251 19 xpdom2 
 |-  ( { (/) } ~<_ a -> ( a X. { (/) } ) ~<_ ( a X. a ) )
252 endomtr 
 |-  ( ( a ~~ ( a X. { (/) } ) /\ ( a X. { (/) } ) ~<_ ( a X. a ) ) -> a ~<_ ( a X. a ) )
253 250 251 252 sylancr 
 |-  ( { (/) } ~<_ a -> a ~<_ ( a X. a ) )
254 247 253 syl 
 |-  ( _om C_ a -> a ~<_ ( a X. a ) )
255 254 ad2antrl 
 |-  ( ( ( 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 ) )
256 sbth 
 |-  ( ( ( a X. a ) ~<_ a /\ a ~<_ ( a X. a ) ) -> ( a X. a ) ~~ a )
257 239 255 256 syl2anc 
 |-  ( ( ( 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 )
258 257 expr 
 |-  ( ( ( 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 ) )
259 simplr 
 |-  ( ( ( 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 ) )
260 simpll 
 |-  ( ( ( 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 )
261 simprr 
 |-  ( ( ( 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 )
262 rexnal 
 |-  ( E. m e. a -. m ~< a <-> -. A. m e. a m ~< a )
263 onelss 
 |-  ( a e. On -> ( m e. a -> m C_ a ) )
264 ssdomg 
 |-  ( a e. On -> ( m C_ a -> m ~<_ a ) )
265 263 264 syld 
 |-  ( a e. On -> ( m e. a -> m ~<_ a ) )
266 bren2 
 |-  ( m ~~ a <-> ( m ~<_ a /\ -. m ~< a ) )
267 266 simplbi2 
 |-  ( m ~<_ a -> ( -. m ~< a -> m ~~ a ) )
268 265 267 syl6 
 |-  ( a e. On -> ( m e. a -> ( -. m ~< a -> m ~~ a ) ) )
269 268 reximdvai 
 |-  ( a e. On -> ( E. m e. a -. m ~< a -> E. m e. a m ~~ a ) )
270 262 269 syl5bir 
 |-  ( a e. On -> ( -. A. m e. a m ~< a -> E. m e. a m ~~ a ) )
271 260 261 270 sylc 
 |-  ( ( ( 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 )
272 r19.29 
 |-  ( ( 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 ) )
273 259 271 272 syl2anc 
 |-  ( ( ( 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 ) )
274 simprl 
 |-  ( ( ( 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 )
275 onelon 
 |-  ( ( a e. On /\ m e. a ) -> m e. On )
276 ensym 
 |-  ( m ~~ a -> a ~~ m )
277 domentr 
 |-  ( ( _om ~<_ a /\ a ~~ m ) -> _om ~<_ m )
278 191 276 277 syl2an 
 |-  ( ( _om C_ a /\ m ~~ a ) -> _om ~<_ m )
279 domnsym 
 |-  ( _om ~<_ m -> -. m ~< _om )
280 nnsdom 
 |-  ( m e. _om -> m ~< _om )
281 279 280 nsyl 
 |-  ( _om ~<_ m -> -. m e. _om )
282 ontri1 
 |-  ( ( _om e. On /\ m e. On ) -> ( _om C_ m <-> -. m e. _om ) )
283 199 282 mpan 
 |-  ( m e. On -> ( _om C_ m <-> -. m e. _om ) )
284 281 283 syl5ibr 
 |-  ( m e. On -> ( _om ~<_ m -> _om C_ m ) )
285 275 278 284 syl2im 
 |-  ( ( a e. On /\ m e. a ) -> ( ( _om C_ a /\ m ~~ a ) -> _om C_ m ) )
286 285 expd 
 |-  ( ( a e. On /\ m e. a ) -> ( _om C_ a -> ( m ~~ a -> _om C_ m ) ) )
287 286 impcom 
 |-  ( ( _om C_ a /\ ( a e. On /\ m e. a ) ) -> ( m ~~ a -> _om C_ m ) )
288 287 imim1d 
 |-  ( ( _om C_ a /\ ( a e. On /\ m e. a ) ) -> ( ( _om C_ m -> ( m X. m ) ~~ m ) -> ( m ~~ a -> ( m X. m ) ~~ m ) ) )
289 288 imp32 
 |-  ( ( ( _om C_ a /\ ( a e. On /\ m e. a ) ) /\ ( ( _om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) ) -> ( m X. m ) ~~ m )
290 entr 
 |-  ( ( ( m X. m ) ~~ m /\ m ~~ a ) -> ( m X. m ) ~~ a )
291 290 ancoms 
 |-  ( ( m ~~ a /\ ( m X. m ) ~~ m ) -> ( m X. m ) ~~ a )
292 xpen 
 |-  ( ( a ~~ m /\ a ~~ m ) -> ( a X. a ) ~~ ( m X. m ) )
293 292 anidms 
 |-  ( a ~~ m -> ( a X. a ) ~~ ( m X. m ) )
294 entr 
 |-  ( ( ( a X. a ) ~~ ( m X. m ) /\ ( m X. m ) ~~ a ) -> ( a X. a ) ~~ a )
295 293 294 sylan 
 |-  ( ( a ~~ m /\ ( m X. m ) ~~ a ) -> ( a X. a ) ~~ a )
296 276 291 295 syl2an2r 
 |-  ( ( m ~~ a /\ ( m X. m ) ~~ m ) -> ( a X. a ) ~~ a )
297 296 ex 
 |-  ( m ~~ a -> ( ( m X. m ) ~~ m -> ( a X. a ) ~~ a ) )
298 297 ad2antll 
 |-  ( ( ( _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 ) )
299 289 298 mpd 
 |-  ( ( ( _om C_ a /\ ( a e. On /\ m e. a ) ) /\ ( ( _om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) ) -> ( a X. a ) ~~ a )
300 299 ex 
 |-  ( ( _om C_ a /\ ( a e. On /\ m e. a ) ) -> ( ( ( _om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) -> ( a X. a ) ~~ a ) )
301 300 expr 
 |-  ( ( _om C_ a /\ a e. On ) -> ( m e. a -> ( ( ( _om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) -> ( a X. a ) ~~ a ) ) )
302 301 rexlimdv 
 |-  ( ( _om C_ a /\ a e. On ) -> ( E. m e. a ( ( _om C_ m -> ( m X. m ) ~~ m ) /\ m ~~ a ) -> ( a X. a ) ~~ a ) )
303 274 260 302 syl2anc 
 |-  ( ( ( 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 ) )
304 273 303 mpd 
 |-  ( ( ( 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 )
305 304 expr 
 |-  ( ( ( 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 ) )
306 258 305 pm2.61d 
 |-  ( ( ( a e. On /\ A. m e. a ( _om C_ m -> ( m X. m ) ~~ m ) ) /\ _om C_ a ) -> ( a X. a ) ~~ a )
307 306 exp31 
 |-  ( a e. On -> ( A. m e. a ( _om C_ m -> ( m X. m ) ~~ m ) -> ( _om C_ a -> ( a X. a ) ~~ a ) ) )
308 12 18 307 tfis3 
 |-  ( A e. On -> ( _om C_ A -> ( A X. A ) ~~ A ) )
309 308 imp 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A X. A ) ~~ A )