Metamath Proof Explorer

Theorem inar1

Description: ( R1A ) for A a strongly inaccessible cardinal is equipotent to A . (Contributed by Mario Carneiro, 6-Jun-2013)

Ref Expression
Assertion inar1 
|- ( A e. Inacc -> ( R1 ` A ) ~~ A )

Proof

Step Hyp Ref Expression
1 inawina 
 |-  ( A e. Inacc -> A e. InaccW )
2 winaon 
 |-  ( A e. InaccW -> A e. On )
3 1 2 syl 
 |-  ( A e. Inacc -> A e. On )
4 winalim 
 |-  ( A e. InaccW -> Lim A )
5 1 4 syl 
 |-  ( A e. Inacc -> Lim A )
6 r1lim 
 |-  ( ( A e. On /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) )
7 3 5 6 syl2anc 
 |-  ( A e. Inacc -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) )
8 onelon 
 |-  ( ( A e. On /\ x e. A ) -> x e. On )
9 3 8 sylan 
 |-  ( ( A e. Inacc /\ x e. A ) -> x e. On )
10 eleq1 
 |-  ( x = (/) -> ( x e. A <-> (/) e. A ) )
11 fveq2 
 |-  ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
12 11 breq1d 
 |-  ( x = (/) -> ( ( R1 ` x ) ~< A <-> ( R1 ` (/) ) ~< A ) )
13 10 12 imbi12d 
 |-  ( x = (/) -> ( ( x e. A -> ( R1 ` x ) ~< A ) <-> ( (/) e. A -> ( R1 ` (/) ) ~< A ) ) )
14 eleq1 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
15 fveq2 
 |-  ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
16 15 breq1d 
 |-  ( x = y -> ( ( R1 ` x ) ~< A <-> ( R1 ` y ) ~< A ) )
17 14 16 imbi12d 
 |-  ( x = y -> ( ( x e. A -> ( R1 ` x ) ~< A ) <-> ( y e. A -> ( R1 ` y ) ~< A ) ) )
18 eleq1 
 |-  ( x = suc y -> ( x e. A <-> suc y e. A ) )
19 fveq2 
 |-  ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
20 19 breq1d 
 |-  ( x = suc y -> ( ( R1 ` x ) ~< A <-> ( R1 ` suc y ) ~< A ) )
21 18 20 imbi12d 
 |-  ( x = suc y -> ( ( x e. A -> ( R1 ` x ) ~< A ) <-> ( suc y e. A -> ( R1 ` suc y ) ~< A ) ) )
22 ne0i 
 |-  ( (/) e. A -> A =/= (/) )
23 0sdomg 
 |-  ( A e. On -> ( (/) ~< A <-> A =/= (/) ) )
24 22 23 imbitrrid 
 |-  ( A e. On -> ( (/) e. A -> (/) ~< A ) )
25 r10 
 |-  ( R1 ` (/) ) = (/)
26 25 breq1i 
 |-  ( ( R1 ` (/) ) ~< A <-> (/) ~< A )
27 24 26 imbitrrdi 
 |-  ( A e. On -> ( (/) e. A -> ( R1 ` (/) ) ~< A ) )
28 1 2 27 3syl 
 |-  ( A e. Inacc -> ( (/) e. A -> ( R1 ` (/) ) ~< A ) )
29 eloni 
 |-  ( A e. On -> Ord A )
30 ordtr 
 |-  ( Ord A -> Tr A )
31 29 30 syl 
 |-  ( A e. On -> Tr A )
32 trsuc 
 |-  ( ( Tr A /\ suc y e. A ) -> y e. A )
33 32 ex 
 |-  ( Tr A -> ( suc y e. A -> y e. A ) )
34 3 31 33 3syl 
 |-  ( A e. Inacc -> ( suc y e. A -> y e. A ) )
35 34 adantl 
 |-  ( ( y e. On /\ A e. Inacc ) -> ( suc y e. A -> y e. A ) )
36 r1suc 
 |-  ( y e. On -> ( R1 ` suc y ) = ~P ( R1 ` y ) )
37 fvex 
 |-  ( R1 ` y ) e. _V
38 37 cardid 
 |-  ( card ` ( R1 ` y ) ) ~~ ( R1 ` y )
39 38 ensymi 
 |-  ( R1 ` y ) ~~ ( card ` ( R1 ` y ) )
40 pwen 
 |-  ( ( R1 ` y ) ~~ ( card ` ( R1 ` y ) ) -> ~P ( R1 ` y ) ~~ ~P ( card ` ( R1 ` y ) ) )
41 39 40 ax-mp 
 |-  ~P ( R1 ` y ) ~~ ~P ( card ` ( R1 ` y ) )
42 36 41 eqbrtrdi 
 |-  ( y e. On -> ( R1 ` suc y ) ~~ ~P ( card ` ( R1 ` y ) ) )
43 winacard 
 |-  ( A e. InaccW -> ( card ` A ) = A )
44 43 eleq2d 
 |-  ( A e. InaccW -> ( ( card ` ( R1 ` y ) ) e. ( card ` A ) <-> ( card ` ( R1 ` y ) ) e. A ) )
45 cardsdom 
 |-  ( ( ( R1 ` y ) e. _V /\ A e. On ) -> ( ( card ` ( R1 ` y ) ) e. ( card ` A ) <-> ( R1 ` y ) ~< A ) )
46 37 2 45 sylancr 
 |-  ( A e. InaccW -> ( ( card ` ( R1 ` y ) ) e. ( card ` A ) <-> ( R1 ` y ) ~< A ) )
47 44 46 bitr3d 
 |-  ( A e. InaccW -> ( ( card ` ( R1 ` y ) ) e. A <-> ( R1 ` y ) ~< A ) )
48 1 47 syl 
 |-  ( A e. Inacc -> ( ( card ` ( R1 ` y ) ) e. A <-> ( R1 ` y ) ~< A ) )
49 elina 
 |-  ( A e. Inacc <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. z e. A ~P z ~< A ) )
50 49 simp3bi 
 |-  ( A e. Inacc -> A. z e. A ~P z ~< A )
51 pweq 
 |-  ( z = ( card ` ( R1 ` y ) ) -> ~P z = ~P ( card ` ( R1 ` y ) ) )
52 51 breq1d 
 |-  ( z = ( card ` ( R1 ` y ) ) -> ( ~P z ~< A <-> ~P ( card ` ( R1 ` y ) ) ~< A ) )
53 52 rspccv 
 |-  ( A. z e. A ~P z ~< A -> ( ( card ` ( R1 ` y ) ) e. A -> ~P ( card ` ( R1 ` y ) ) ~< A ) )
54 50 53 syl 
 |-  ( A e. Inacc -> ( ( card ` ( R1 ` y ) ) e. A -> ~P ( card ` ( R1 ` y ) ) ~< A ) )
55 48 54 sylbird 
 |-  ( A e. Inacc -> ( ( R1 ` y ) ~< A -> ~P ( card ` ( R1 ` y ) ) ~< A ) )
56 55 imp 
 |-  ( ( A e. Inacc /\ ( R1 ` y ) ~< A ) -> ~P ( card ` ( R1 ` y ) ) ~< A )
57 ensdomtr 
 |-  ( ( ( R1 ` suc y ) ~~ ~P ( card ` ( R1 ` y ) ) /\ ~P ( card ` ( R1 ` y ) ) ~< A ) -> ( R1 ` suc y ) ~< A )
58 42 56 57 syl2an 
 |-  ( ( y e. On /\ ( A e. Inacc /\ ( R1 ` y ) ~< A ) ) -> ( R1 ` suc y ) ~< A )
59 58 expr 
 |-  ( ( y e. On /\ A e. Inacc ) -> ( ( R1 ` y ) ~< A -> ( R1 ` suc y ) ~< A ) )
60 35 59 imim12d 
 |-  ( ( y e. On /\ A e. Inacc ) -> ( ( y e. A -> ( R1 ` y ) ~< A ) -> ( suc y e. A -> ( R1 ` suc y ) ~< A ) ) )
61 60 ex 
 |-  ( y e. On -> ( A e. Inacc -> ( ( y e. A -> ( R1 ` y ) ~< A ) -> ( suc y e. A -> ( R1 ` suc y ) ~< A ) ) ) )
62 vex 
 |-  x e. _V
63 r1lim 
 |-  ( ( x e. _V /\ Lim x ) -> ( R1 ` x ) = U_ z e. x ( R1 ` z ) )
64 62 63 mpan 
 |-  ( Lim x -> ( R1 ` x ) = U_ z e. x ( R1 ` z ) )
65 nfcv 
 |-  F/_ y z
66 nfcv 
 |-  F/_ y ( R1 ` z )
67 nfcv 
 |-  F/_ y ~<_
68 nfiu1 
 |-  F/_ y U_ y e. x ( card ` ( R1 ` y ) )
69 66 67 68 nfbr 
 |-  F/ y ( R1 ` z ) ~<_ U_ y e. x ( card ` ( R1 ` y ) )
70 fveq2 
 |-  ( y = z -> ( R1 ` y ) = ( R1 ` z ) )
71 70 breq1d 
 |-  ( y = z -> ( ( R1 ` y ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) <-> ( R1 ` z ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) ) )
72 fvex 
 |-  ( card ` ( R1 ` y ) ) e. _V
73 62 72 iunex 
 |-  U_ y e. x ( card ` ( R1 ` y ) ) e. _V
74 ssiun2 
 |-  ( y e. x -> ( card ` ( R1 ` y ) ) C_ U_ y e. x ( card ` ( R1 ` y ) ) )
75 ssdomg 
 |-  ( U_ y e. x ( card ` ( R1 ` y ) ) e. _V -> ( ( card ` ( R1 ` y ) ) C_ U_ y e. x ( card ` ( R1 ` y ) ) -> ( card ` ( R1 ` y ) ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) ) )
76 73 74 75 mpsyl 
 |-  ( y e. x -> ( card ` ( R1 ` y ) ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) )
77 endomtr 
 |-  ( ( ( R1 ` y ) ~~ ( card ` ( R1 ` y ) ) /\ ( card ` ( R1 ` y ) ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( R1 ` y ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) )
78 39 76 77 sylancr 
 |-  ( y e. x -> ( R1 ` y ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) )
79 65 69 71 78 vtoclgaf 
 |-  ( z e. x -> ( R1 ` z ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) )
80 79 rgen 
 |-  A. z e. x ( R1 ` z ) ~<_ U_ y e. x ( card ` ( R1 ` y ) )
81 iundom 
 |-  ( ( x e. _V /\ A. z e. x ( R1 ` z ) ~<_ U_ y e. x ( card ` ( R1 ` y ) ) ) -> U_ z e. x ( R1 ` z ) ~<_ ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) )
82 62 80 81 mp2an 
 |-  U_ z e. x ( R1 ` z ) ~<_ ( x X. U_ y e. x ( card ` ( R1 ` y ) ) )
83 62 73 unex 
 |-  ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. _V
84 ssun2 
 |-  U_ y e. x ( card ` ( R1 ` y ) ) C_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) )
85 ssdomg 
 |-  ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. _V -> ( U_ y e. x ( card ` ( R1 ` y ) ) C_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> U_ y e. x ( card ` ( R1 ` y ) ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
86 83 84 85 mp2 
 |-  U_ y e. x ( card ` ( R1 ` y ) ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) )
87 62 xpdom2 
 |-  ( U_ y e. x ( card ` ( R1 ` y ) ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( x X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
88 86 87 ax-mp 
 |-  ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( x X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
89 ssun1 
 |-  x C_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) )
90 ssdomg 
 |-  ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. _V -> ( x C_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> x ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
91 83 89 90 mp2 
 |-  x ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) )
92 83 xpdom1 
 |-  ( x ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( x X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) ~<_ ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
93 91 92 ax-mp 
 |-  ( x X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) ~<_ ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
94 domtr 
 |-  ( ( ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( x X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) /\ ( x X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) ~<_ ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) ) -> ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
95 88 93 94 mp2an 
 |-  ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
96 limomss 
 |-  ( Lim x -> _om C_ x )
97 96 89 sstrdi 
 |-  ( Lim x -> _om C_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
98 ssdomg 
 |-  ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. _V -> ( _om C_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> _om ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
99 83 97 98 mpsyl 
 |-  ( Lim x -> _om ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
100 infxpidm 
 |-  ( _om ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) ~~ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
101 99 100 syl 
 |-  ( Lim x -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) ~~ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
102 domentr 
 |-  ( ( ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) /\ ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) X. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) ~~ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) -> ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
103 95 101 102 sylancr 
 |-  ( Lim x -> ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
104 domtr 
 |-  ( ( U_ z e. x ( R1 ` z ) ~<_ ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) /\ ( x X. U_ y e. x ( card ` ( R1 ` y ) ) ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ) -> U_ z e. x ( R1 ` z ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
105 82 103 104 sylancr 
 |-  ( Lim x -> U_ z e. x ( R1 ` z ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
106 64 105 eqbrtrd 
 |-  ( Lim x -> ( R1 ` x ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
107 106 ad2antlr 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( R1 ` x ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
108 eleq1a 
 |-  ( x e. A -> ( A = x -> A e. A ) )
109 ordirr 
 |-  ( Ord A -> -. A e. A )
110 3 29 109 3syl 
 |-  ( A e. Inacc -> -. A e. A )
111 108 110 nsyli 
 |-  ( x e. A -> ( A e. Inacc -> -. A = x ) )
112 111 imp 
 |-  ( ( x e. A /\ A e. Inacc ) -> -. A = x )
113 112 ad2ant2r 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> -. A = x )
114 simpll 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> x e. A )
115 limord 
 |-  ( Lim x -> Ord x )
116 62 elon 
 |-  ( x e. On <-> Ord x )
117 115 116 sylibr 
 |-  ( Lim x -> x e. On )
118 117 ad2antlr 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> x e. On )
119 cardf 
 |-  card : _V --> On
120 r1fnon 
 |-  R1 Fn On
121 dffn2 
 |-  ( R1 Fn On <-> R1 : On --> _V )
122 120 121 mpbi 
 |-  R1 : On --> _V
123 fco 
 |-  ( ( card : _V --> On /\ R1 : On --> _V ) -> ( card o. R1 ) : On --> On )
124 119 122 123 mp2an 
 |-  ( card o. R1 ) : On --> On
125 onss 
 |-  ( x e. On -> x C_ On )
126 fssres 
 |-  ( ( ( card o. R1 ) : On --> On /\ x C_ On ) -> ( ( card o. R1 ) |` x ) : x --> On )
127 124 125 126 sylancr 
 |-  ( x e. On -> ( ( card o. R1 ) |` x ) : x --> On )
128 ffn 
 |-  ( ( ( card o. R1 ) |` x ) : x --> On -> ( ( card o. R1 ) |` x ) Fn x )
129 118 127 128 3syl 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( ( card o. R1 ) |` x ) Fn x )
130 3 ad2antlr 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> A e. On )
131 simpr 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> y e. x )
132 simplll 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> x e. A )
133 ontr1 
 |-  ( A e. On -> ( ( y e. x /\ x e. A ) -> y e. A ) )
134 133 imp 
 |-  ( ( A e. On /\ ( y e. x /\ x e. A ) ) -> y e. A )
135 130 131 132 134 syl12anc 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> y e. A )
136 37 130 45 sylancr 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( card ` ( R1 ` y ) ) e. ( card ` A ) <-> ( R1 ` y ) ~< A ) )
137 1 43 syl 
 |-  ( A e. Inacc -> ( card ` A ) = A )
138 137 ad2antlr 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( card ` A ) = A )
139 138 eleq2d 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( card ` ( R1 ` y ) ) e. ( card ` A ) <-> ( card ` ( R1 ` y ) ) e. A ) )
140 136 139 bitr3d 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( R1 ` y ) ~< A <-> ( card ` ( R1 ` y ) ) e. A ) )
141 140 biimpd 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( R1 ` y ) ~< A -> ( card ` ( R1 ` y ) ) e. A ) )
142 135 141 embantd 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( y e. A -> ( R1 ` y ) ~< A ) -> ( card ` ( R1 ` y ) ) e. A ) )
143 117 ad2antlr 
 |-  ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) -> x e. On )
144 fvres 
 |-  ( y e. x -> ( ( ( card o. R1 ) |` x ) ` y ) = ( ( card o. R1 ) ` y ) )
145 144 adantl 
 |-  ( ( x e. On /\ y e. x ) -> ( ( ( card o. R1 ) |` x ) ` y ) = ( ( card o. R1 ) ` y ) )
146 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
147 fvco3 
 |-  ( ( R1 : On --> _V /\ y e. On ) -> ( ( card o. R1 ) ` y ) = ( card ` ( R1 ` y ) ) )
148 122 146 147 sylancr 
 |-  ( ( x e. On /\ y e. x ) -> ( ( card o. R1 ) ` y ) = ( card ` ( R1 ` y ) ) )
149 145 148 eqtrd 
 |-  ( ( x e. On /\ y e. x ) -> ( ( ( card o. R1 ) |` x ) ` y ) = ( card ` ( R1 ` y ) ) )
150 143 149 sylan 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( ( card o. R1 ) |` x ) ` y ) = ( card ` ( R1 ` y ) ) )
151 150 eleq1d 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( ( ( card o. R1 ) |` x ) ` y ) e. A <-> ( card ` ( R1 ` y ) ) e. A ) )
152 142 151 sylibrd 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( y e. A -> ( R1 ` y ) ~< A ) -> ( ( ( card o. R1 ) |` x ) ` y ) e. A ) )
153 152 ralimdva 
 |-  ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) -> ( A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) -> A. y e. x ( ( ( card o. R1 ) |` x ) ` y ) e. A ) )
154 153 impr 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> A. y e. x ( ( ( card o. R1 ) |` x ) ` y ) e. A )
155 ffnfv 
 |-  ( ( ( card o. R1 ) |` x ) : x --> A <-> ( ( ( card o. R1 ) |` x ) Fn x /\ A. y e. x ( ( ( card o. R1 ) |` x ) ` y ) e. A ) )
156 129 154 155 sylanbrc 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( ( card o. R1 ) |` x ) : x --> A )
157 eleq2 
 |-  ( A = U_ y e. x ( card ` ( R1 ` y ) ) -> ( z e. A <-> z e. U_ y e. x ( card ` ( R1 ` y ) ) ) )
158 157 biimpa 
 |-  ( ( A = U_ y e. x ( card ` ( R1 ` y ) ) /\ z e. A ) -> z e. U_ y e. x ( card ` ( R1 ` y ) ) )
159 eliun 
 |-  ( z e. U_ y e. x ( card ` ( R1 ` y ) ) <-> E. y e. x z e. ( card ` ( R1 ` y ) ) )
160 cardon 
 |-  ( card ` ( R1 ` y ) ) e. On
161 160 onelssi 
 |-  ( z e. ( card ` ( R1 ` y ) ) -> z C_ ( card ` ( R1 ` y ) ) )
162 149 sseq2d 
 |-  ( ( x e. On /\ y e. x ) -> ( z C_ ( ( ( card o. R1 ) |` x ) ` y ) <-> z C_ ( card ` ( R1 ` y ) ) ) )
163 161 162 imbitrrid 
 |-  ( ( x e. On /\ y e. x ) -> ( z e. ( card ` ( R1 ` y ) ) -> z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
164 163 reximdva 
 |-  ( x e. On -> ( E. y e. x z e. ( card ` ( R1 ` y ) ) -> E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
165 159 164 biimtrid 
 |-  ( x e. On -> ( z e. U_ y e. x ( card ` ( R1 ` y ) ) -> E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
166 158 165 syl5 
 |-  ( x e. On -> ( ( A = U_ y e. x ( card ` ( R1 ` y ) ) /\ z e. A ) -> E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
167 166 expdimp 
 |-  ( ( x e. On /\ A = U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( z e. A -> E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
168 167 ralrimiv 
 |-  ( ( x e. On /\ A = U_ y e. x ( card ` ( R1 ` y ) ) ) -> A. z e. A E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) )
169 168 ex 
 |-  ( x e. On -> ( A = U_ y e. x ( card ` ( R1 ` y ) ) -> A. z e. A E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
170 118 169 syl 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( A = U_ y e. x ( card ` ( R1 ` y ) ) -> A. z e. A E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
171 ffun 
 |-  ( ( card o. R1 ) : On --> On -> Fun ( card o. R1 ) )
172 124 171 ax-mp 
 |-  Fun ( card o. R1 )
173 resfunexg 
 |-  ( ( Fun ( card o. R1 ) /\ x e. _V ) -> ( ( card o. R1 ) |` x ) e. _V )
174 172 62 173 mp2an 
 |-  ( ( card o. R1 ) |` x ) e. _V
175 feq1 
 |-  ( w = ( ( card o. R1 ) |` x ) -> ( w : x --> A <-> ( ( card o. R1 ) |` x ) : x --> A ) )
176 fveq1 
 |-  ( w = ( ( card o. R1 ) |` x ) -> ( w ` y ) = ( ( ( card o. R1 ) |` x ) ` y ) )
177 176 sseq2d 
 |-  ( w = ( ( card o. R1 ) |` x ) -> ( z C_ ( w ` y ) <-> z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
178 177 rexbidv 
 |-  ( w = ( ( card o. R1 ) |` x ) -> ( E. y e. x z C_ ( w ` y ) <-> E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
179 178 ralbidv 
 |-  ( w = ( ( card o. R1 ) |` x ) -> ( A. z e. A E. y e. x z C_ ( w ` y ) <-> A. z e. A E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) )
180 175 179 anbi12d 
 |-  ( w = ( ( card o. R1 ) |` x ) -> ( ( w : x --> A /\ A. z e. A E. y e. x z C_ ( w ` y ) ) <-> ( ( ( card o. R1 ) |` x ) : x --> A /\ A. z e. A E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) ) )
181 174 180 spcev 
 |-  ( ( ( ( card o. R1 ) |` x ) : x --> A /\ A. z e. A E. y e. x z C_ ( ( ( card o. R1 ) |` x ) ` y ) ) -> E. w ( w : x --> A /\ A. z e. A E. y e. x z C_ ( w ` y ) ) )
182 156 170 181 syl6an 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( A = U_ y e. x ( card ` ( R1 ` y ) ) -> E. w ( w : x --> A /\ A. z e. A E. y e. x z C_ ( w ` y ) ) ) )
183 3 ad2antrl 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> A e. On )
184 cfflb 
 |-  ( ( A e. On /\ x e. On ) -> ( E. w ( w : x --> A /\ A. z e. A E. y e. x z C_ ( w ` y ) ) -> ( cf ` A ) C_ x ) )
185 183 118 184 syl2anc 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( E. w ( w : x --> A /\ A. z e. A E. y e. x z C_ ( w ` y ) ) -> ( cf ` A ) C_ x ) )
186 182 185 syld 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( A = U_ y e. x ( card ` ( R1 ` y ) ) -> ( cf ` A ) C_ x ) )
187 49 simp2bi 
 |-  ( A e. Inacc -> ( cf ` A ) = A )
188 187 sseq1d 
 |-  ( A e. Inacc -> ( ( cf ` A ) C_ x <-> A C_ x ) )
189 188 ad2antrl 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( ( cf ` A ) C_ x <-> A C_ x ) )
190 186 189 sylibd 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( A = U_ y e. x ( card ` ( R1 ` y ) ) -> A C_ x ) )
191 ontri1 
 |-  ( ( A e. On /\ x e. On ) -> ( A C_ x <-> -. x e. A ) )
192 183 118 191 syl2anc 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( A C_ x <-> -. x e. A ) )
193 190 192 sylibd 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( A = U_ y e. x ( card ` ( R1 ` y ) ) -> -. x e. A ) )
194 114 193 mt2d 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> -. A = U_ y e. x ( card ` ( R1 ` y ) ) )
195 iunon 
 |-  ( ( x e. _V /\ A. y e. x ( card ` ( R1 ` y ) ) e. On ) -> U_ y e. x ( card ` ( R1 ` y ) ) e. On )
196 62 195 mpan 
 |-  ( A. y e. x ( card ` ( R1 ` y ) ) e. On -> U_ y e. x ( card ` ( R1 ` y ) ) e. On )
197 160 a1i 
 |-  ( y e. x -> ( card ` ( R1 ` y ) ) e. On )
198 196 197 mprg 
 |-  U_ y e. x ( card ` ( R1 ` y ) ) e. On
199 eqcom 
 |-  ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A <-> A = ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) )
200 eloni 
 |-  ( x e. On -> Ord x )
201 eloni 
 |-  ( U_ y e. x ( card ` ( R1 ` y ) ) e. On -> Ord U_ y e. x ( card ` ( R1 ` y ) ) )
202 ordequn 
 |-  ( ( Ord x /\ Ord U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( A = ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( A = x \/ A = U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
203 200 201 202 syl2an 
 |-  ( ( x e. On /\ U_ y e. x ( card ` ( R1 ` y ) ) e. On ) -> ( A = ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( A = x \/ A = U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
204 199 203 biimtrid 
 |-  ( ( x e. On /\ U_ y e. x ( card ` ( R1 ` y ) ) e. On ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A -> ( A = x \/ A = U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
205 118 198 204 sylancl 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A -> ( A = x \/ A = U_ y e. x ( card ` ( R1 ` y ) ) ) ) )
206 113 194 205 mtord 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> -. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A )
207 onelss 
 |-  ( A e. On -> ( x e. A -> x C_ A ) )
208 183 114 207 sylc 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> x C_ A )
209 onelss 
 |-  ( A e. On -> ( ( card ` ( R1 ` y ) ) e. A -> ( card ` ( R1 ` y ) ) C_ A ) )
210 130 142 209 sylsyld 
 |-  ( ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) /\ y e. x ) -> ( ( y e. A -> ( R1 ` y ) ~< A ) -> ( card ` ( R1 ` y ) ) C_ A ) )
211 210 ralimdva 
 |-  ( ( ( x e. A /\ Lim x ) /\ A e. Inacc ) -> ( A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) -> A. y e. x ( card ` ( R1 ` y ) ) C_ A ) )
212 211 impr 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> A. y e. x ( card ` ( R1 ` y ) ) C_ A )
213 iunss 
 |-  ( U_ y e. x ( card ` ( R1 ` y ) ) C_ A <-> A. y e. x ( card ` ( R1 ` y ) ) C_ A )
214 212 213 sylibr 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> U_ y e. x ( card ` ( R1 ` y ) ) C_ A )
215 208 214 unssd 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) C_ A )
216 id 
 |-  ( x = if ( x e. On , x , (/) ) -> x = if ( x e. On , x , (/) ) )
217 iuneq1 
 |-  ( x = if ( x e. On , x , (/) ) -> U_ y e. x ( card ` ( R1 ` y ) ) = U_ y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) )
218 216 217 uneq12d 
 |-  ( x = if ( x e. On , x , (/) ) -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = ( if ( x e. On , x , (/) ) u. U_ y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) ) )
219 218 eleq1d 
 |-  ( x = if ( x e. On , x , (/) ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. On <-> ( if ( x e. On , x , (/) ) u. U_ y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) ) e. On ) )
220 0elon 
 |-  (/) e. On
221 220 elimel 
 |-  if ( x e. On , x , (/) ) e. On
222 221 elexi 
 |-  if ( x e. On , x , (/) ) e. _V
223 iunon 
 |-  ( ( if ( x e. On , x , (/) ) e. _V /\ A. y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) e. On ) -> U_ y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) e. On )
224 222 223 mpan 
 |-  ( A. y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) e. On -> U_ y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) e. On )
225 160 a1i 
 |-  ( y e. if ( x e. On , x , (/) ) -> ( card ` ( R1 ` y ) ) e. On )
226 224 225 mprg 
 |-  U_ y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) e. On
227 221 226 onun2i 
 |-  ( if ( x e. On , x , (/) ) u. U_ y e. if ( x e. On , x , (/) ) ( card ` ( R1 ` y ) ) ) e. On
228 219 227 dedth 
 |-  ( x e. On -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. On )
229 117 228 syl 
 |-  ( Lim x -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. On )
230 229 adantl 
 |-  ( ( x e. A /\ Lim x ) -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. On )
231 3 adantr 
 |-  ( ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) -> A e. On )
232 onsseleq 
 |-  ( ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. On /\ A e. On ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) C_ A <-> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. A \/ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A ) ) )
233 230 231 232 syl2an 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) C_ A <-> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. A \/ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A ) ) )
234 215 233 mpbid 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. A \/ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A ) )
235 234 orcomd 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A \/ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. A ) )
236 235 ord 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( -. ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) = A -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. A ) )
237 206 236 mpd 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. A )
238 137 ad2antrl 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( card ` A ) = A )
239 iscard 
 |-  ( ( card ` A ) = A <-> ( A e. On /\ A. z e. A z ~< A ) )
240 239 simprbi 
 |-  ( ( card ` A ) = A -> A. z e. A z ~< A )
241 breq1 
 |-  ( z = ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) -> ( z ~< A <-> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ~< A ) )
242 241 rspccv 
 |-  ( A. z e. A z ~< A -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. A -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ~< A ) )
243 238 240 242 3syl 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) e. A -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ~< A ) )
244 237 243 mpd 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ~< A )
245 domsdomtr 
 |-  ( ( ( R1 ` x ) ~<_ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) /\ ( x u. U_ y e. x ( card ` ( R1 ` y ) ) ) ~< A ) -> ( R1 ` x ) ~< A )
246 107 244 245 syl2anc 
 |-  ( ( ( x e. A /\ Lim x ) /\ ( A e. Inacc /\ A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) ) ) -> ( R1 ` x ) ~< A )
247 246 exp43 
 |-  ( x e. A -> ( Lim x -> ( A e. Inacc -> ( A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) -> ( R1 ` x ) ~< A ) ) ) )
248 247 com4l 
 |-  ( Lim x -> ( A e. Inacc -> ( A. y e. x ( y e. A -> ( R1 ` y ) ~< A ) -> ( x e. A -> ( R1 ` x ) ~< A ) ) ) )
249 13 17 21 28 61 248 tfinds2 
 |-  ( x e. On -> ( A e. Inacc -> ( x e. A -> ( R1 ` x ) ~< A ) ) )
250 249 impd 
 |-  ( x e. On -> ( ( A e. Inacc /\ x e. A ) -> ( R1 ` x ) ~< A ) )
251 9 250 mpcom 
 |-  ( ( A e. Inacc /\ x e. A ) -> ( R1 ` x ) ~< A )
252 sdomdom 
 |-  ( ( R1 ` x ) ~< A -> ( R1 ` x ) ~<_ A )
253 251 252 syl 
 |-  ( ( A e. Inacc /\ x e. A ) -> ( R1 ` x ) ~<_ A )
254 253 ralrimiva 
 |-  ( A e. Inacc -> A. x e. A ( R1 ` x ) ~<_ A )
255 iundom 
 |-  ( ( A e. On /\ A. x e. A ( R1 ` x ) ~<_ A ) -> U_ x e. A ( R1 ` x ) ~<_ ( A X. A ) )
256 3 254 255 syl2anc 
 |-  ( A e. Inacc -> U_ x e. A ( R1 ` x ) ~<_ ( A X. A ) )
257 7 256 eqbrtrd 
 |-  ( A e. Inacc -> ( R1 ` A ) ~<_ ( A X. A ) )
258 winainf 
 |-  ( A e. InaccW -> _om C_ A )
259 1 258 syl 
 |-  ( A e. Inacc -> _om C_ A )
260 infxpen 
 |-  ( ( A e. On /\ _om C_ A ) -> ( A X. A ) ~~ A )
261 3 259 260 syl2anc 
 |-  ( A e. Inacc -> ( A X. A ) ~~ A )
262 domentr 
 |-  ( ( ( R1 ` A ) ~<_ ( A X. A ) /\ ( A X. A ) ~~ A ) -> ( R1 ` A ) ~<_ A )
263 257 261 262 syl2anc 
 |-  ( A e. Inacc -> ( R1 ` A ) ~<_ A )
264 fvex 
 |-  ( R1 ` A ) e. _V
265 122 fdmi 
 |-  dom R1 = On
266 2 265 eleqtrrdi 
 |-  ( A e. InaccW -> A e. dom R1 )
267 onssr1 
 |-  ( A e. dom R1 -> A C_ ( R1 ` A ) )
268 1 266 267 3syl 
 |-  ( A e. Inacc -> A C_ ( R1 ` A ) )
269 ssdomg 
 |-  ( ( R1 ` A ) e. _V -> ( A C_ ( R1 ` A ) -> A ~<_ ( R1 ` A ) ) )
270 264 268 269 mpsyl 
 |-  ( A e. Inacc -> A ~<_ ( R1 ` A ) )
271 sbth 
 |-  ( ( ( R1 ` A ) ~<_ A /\ A ~<_ ( R1 ` A ) ) -> ( R1 ` A ) ~~ A )
272 263 270 271 syl2anc 
 |-  ( A e. Inacc -> ( R1 ` A ) ~~ A )