Step |
Hyp |
Ref |
Expression |
1 |
|
oeeu.1 |
|- X = U. |^| { x e. On | B e. ( A ^o x ) } |
2 |
|
eldifi |
|- ( B e. ( On \ 1o ) -> B e. On ) |
3 |
2
|
adantl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B e. On ) |
4 |
|
suceloni |
|- ( B e. On -> suc B e. On ) |
5 |
3 4
|
syl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> suc B e. On ) |
6 |
|
oeworde |
|- ( ( A e. ( On \ 2o ) /\ suc B e. On ) -> suc B C_ ( A ^o suc B ) ) |
7 |
5 6
|
syldan |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> suc B C_ ( A ^o suc B ) ) |
8 |
|
sucidg |
|- ( B e. On -> B e. suc B ) |
9 |
3 8
|
syl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B e. suc B ) |
10 |
7 9
|
sseldd |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B e. ( A ^o suc B ) ) |
11 |
|
oveq2 |
|- ( x = suc B -> ( A ^o x ) = ( A ^o suc B ) ) |
12 |
11
|
eleq2d |
|- ( x = suc B -> ( B e. ( A ^o x ) <-> B e. ( A ^o suc B ) ) ) |
13 |
12
|
rspcev |
|- ( ( suc B e. On /\ B e. ( A ^o suc B ) ) -> E. x e. On B e. ( A ^o x ) ) |
14 |
5 10 13
|
syl2anc |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> E. x e. On B e. ( A ^o x ) ) |
15 |
|
onintrab2 |
|- ( E. x e. On B e. ( A ^o x ) <-> |^| { x e. On | B e. ( A ^o x ) } e. On ) |
16 |
14 15
|
sylib |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> |^| { x e. On | B e. ( A ^o x ) } e. On ) |
17 |
|
onuni |
|- ( |^| { x e. On | B e. ( A ^o x ) } e. On -> U. |^| { x e. On | B e. ( A ^o x ) } e. On ) |
18 |
16 17
|
syl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> U. |^| { x e. On | B e. ( A ^o x ) } e. On ) |
19 |
1 18
|
eqeltrid |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> X e. On ) |
20 |
|
sucidg |
|- ( X e. On -> X e. suc X ) |
21 |
19 20
|
syl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> X e. suc X ) |
22 |
|
suceq |
|- ( X = U. |^| { x e. On | B e. ( A ^o x ) } -> suc X = suc U. |^| { x e. On | B e. ( A ^o x ) } ) |
23 |
1 22
|
ax-mp |
|- suc X = suc U. |^| { x e. On | B e. ( A ^o x ) } |
24 |
|
dif1o |
|- ( B e. ( On \ 1o ) <-> ( B e. On /\ B =/= (/) ) ) |
25 |
24
|
simprbi |
|- ( B e. ( On \ 1o ) -> B =/= (/) ) |
26 |
25
|
adantl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B =/= (/) ) |
27 |
|
ssrab2 |
|- { x e. On | B e. ( A ^o x ) } C_ On |
28 |
|
rabn0 |
|- ( { x e. On | B e. ( A ^o x ) } =/= (/) <-> E. x e. On B e. ( A ^o x ) ) |
29 |
14 28
|
sylibr |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> { x e. On | B e. ( A ^o x ) } =/= (/) ) |
30 |
|
onint |
|- ( ( { x e. On | B e. ( A ^o x ) } C_ On /\ { x e. On | B e. ( A ^o x ) } =/= (/) ) -> |^| { x e. On | B e. ( A ^o x ) } e. { x e. On | B e. ( A ^o x ) } ) |
31 |
27 29 30
|
sylancr |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> |^| { x e. On | B e. ( A ^o x ) } e. { x e. On | B e. ( A ^o x ) } ) |
32 |
|
eleq1 |
|- ( |^| { x e. On | B e. ( A ^o x ) } = (/) -> ( |^| { x e. On | B e. ( A ^o x ) } e. { x e. On | B e. ( A ^o x ) } <-> (/) e. { x e. On | B e. ( A ^o x ) } ) ) |
33 |
31 32
|
syl5ibcom |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( |^| { x e. On | B e. ( A ^o x ) } = (/) -> (/) e. { x e. On | B e. ( A ^o x ) } ) ) |
34 |
|
oveq2 |
|- ( x = (/) -> ( A ^o x ) = ( A ^o (/) ) ) |
35 |
34
|
eleq2d |
|- ( x = (/) -> ( B e. ( A ^o x ) <-> B e. ( A ^o (/) ) ) ) |
36 |
35
|
elrab |
|- ( (/) e. { x e. On | B e. ( A ^o x ) } <-> ( (/) e. On /\ B e. ( A ^o (/) ) ) ) |
37 |
36
|
simprbi |
|- ( (/) e. { x e. On | B e. ( A ^o x ) } -> B e. ( A ^o (/) ) ) |
38 |
|
eldifi |
|- ( A e. ( On \ 2o ) -> A e. On ) |
39 |
38
|
adantr |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> A e. On ) |
40 |
|
oe0 |
|- ( A e. On -> ( A ^o (/) ) = 1o ) |
41 |
39 40
|
syl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o (/) ) = 1o ) |
42 |
41
|
eleq2d |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( B e. ( A ^o (/) ) <-> B e. 1o ) ) |
43 |
|
el1o |
|- ( B e. 1o <-> B = (/) ) |
44 |
42 43
|
bitrdi |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( B e. ( A ^o (/) ) <-> B = (/) ) ) |
45 |
37 44
|
syl5ib |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( (/) e. { x e. On | B e. ( A ^o x ) } -> B = (/) ) ) |
46 |
33 45
|
syld |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( |^| { x e. On | B e. ( A ^o x ) } = (/) -> B = (/) ) ) |
47 |
46
|
necon3ad |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( B =/= (/) -> -. |^| { x e. On | B e. ( A ^o x ) } = (/) ) ) |
48 |
26 47
|
mpd |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> -. |^| { x e. On | B e. ( A ^o x ) } = (/) ) |
49 |
|
limuni |
|- ( Lim |^| { x e. On | B e. ( A ^o x ) } -> |^| { x e. On | B e. ( A ^o x ) } = U. |^| { x e. On | B e. ( A ^o x ) } ) |
50 |
49 1
|
eqtr4di |
|- ( Lim |^| { x e. On | B e. ( A ^o x ) } -> |^| { x e. On | B e. ( A ^o x ) } = X ) |
51 |
50
|
adantl |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> |^| { x e. On | B e. ( A ^o x ) } = X ) |
52 |
31
|
adantr |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> |^| { x e. On | B e. ( A ^o x ) } e. { x e. On | B e. ( A ^o x ) } ) |
53 |
51 52
|
eqeltrrd |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> X e. { x e. On | B e. ( A ^o x ) } ) |
54 |
|
oveq2 |
|- ( y = X -> ( A ^o y ) = ( A ^o X ) ) |
55 |
54
|
eleq2d |
|- ( y = X -> ( B e. ( A ^o y ) <-> B e. ( A ^o X ) ) ) |
56 |
|
oveq2 |
|- ( x = y -> ( A ^o x ) = ( A ^o y ) ) |
57 |
56
|
eleq2d |
|- ( x = y -> ( B e. ( A ^o x ) <-> B e. ( A ^o y ) ) ) |
58 |
57
|
cbvrabv |
|- { x e. On | B e. ( A ^o x ) } = { y e. On | B e. ( A ^o y ) } |
59 |
55 58
|
elrab2 |
|- ( X e. { x e. On | B e. ( A ^o x ) } <-> ( X e. On /\ B e. ( A ^o X ) ) ) |
60 |
59
|
simprbi |
|- ( X e. { x e. On | B e. ( A ^o x ) } -> B e. ( A ^o X ) ) |
61 |
53 60
|
syl |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> B e. ( A ^o X ) ) |
62 |
38
|
ad2antrr |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> A e. On ) |
63 |
|
limeq |
|- ( |^| { x e. On | B e. ( A ^o x ) } = X -> ( Lim |^| { x e. On | B e. ( A ^o x ) } <-> Lim X ) ) |
64 |
50 63
|
syl |
|- ( Lim |^| { x e. On | B e. ( A ^o x ) } -> ( Lim |^| { x e. On | B e. ( A ^o x ) } <-> Lim X ) ) |
65 |
64
|
ibi |
|- ( Lim |^| { x e. On | B e. ( A ^o x ) } -> Lim X ) |
66 |
19 65
|
anim12i |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> ( X e. On /\ Lim X ) ) |
67 |
|
dif20el |
|- ( A e. ( On \ 2o ) -> (/) e. A ) |
68 |
67
|
ad2antrr |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> (/) e. A ) |
69 |
|
oelim |
|- ( ( ( A e. On /\ ( X e. On /\ Lim X ) ) /\ (/) e. A ) -> ( A ^o X ) = U_ y e. X ( A ^o y ) ) |
70 |
62 66 68 69
|
syl21anc |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> ( A ^o X ) = U_ y e. X ( A ^o y ) ) |
71 |
61 70
|
eleqtrd |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> B e. U_ y e. X ( A ^o y ) ) |
72 |
|
eliun |
|- ( B e. U_ y e. X ( A ^o y ) <-> E. y e. X B e. ( A ^o y ) ) |
73 |
71 72
|
sylib |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> E. y e. X B e. ( A ^o y ) ) |
74 |
19
|
adantr |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> X e. On ) |
75 |
|
onss |
|- ( X e. On -> X C_ On ) |
76 |
74 75
|
syl |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> X C_ On ) |
77 |
76
|
sselda |
|- ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) /\ y e. X ) -> y e. On ) |
78 |
51
|
eleq2d |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> ( y e. |^| { x e. On | B e. ( A ^o x ) } <-> y e. X ) ) |
79 |
78
|
biimpar |
|- ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) /\ y e. X ) -> y e. |^| { x e. On | B e. ( A ^o x ) } ) |
80 |
57
|
onnminsb |
|- ( y e. On -> ( y e. |^| { x e. On | B e. ( A ^o x ) } -> -. B e. ( A ^o y ) ) ) |
81 |
77 79 80
|
sylc |
|- ( ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) /\ y e. X ) -> -. B e. ( A ^o y ) ) |
82 |
81
|
nrexdv |
|- ( ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) /\ Lim |^| { x e. On | B e. ( A ^o x ) } ) -> -. E. y e. X B e. ( A ^o y ) ) |
83 |
73 82
|
pm2.65da |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> -. Lim |^| { x e. On | B e. ( A ^o x ) } ) |
84 |
|
ioran |
|- ( -. ( |^| { x e. On | B e. ( A ^o x ) } = (/) \/ Lim |^| { x e. On | B e. ( A ^o x ) } ) <-> ( -. |^| { x e. On | B e. ( A ^o x ) } = (/) /\ -. Lim |^| { x e. On | B e. ( A ^o x ) } ) ) |
85 |
48 83 84
|
sylanbrc |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> -. ( |^| { x e. On | B e. ( A ^o x ) } = (/) \/ Lim |^| { x e. On | B e. ( A ^o x ) } ) ) |
86 |
|
eloni |
|- ( |^| { x e. On | B e. ( A ^o x ) } e. On -> Ord |^| { x e. On | B e. ( A ^o x ) } ) |
87 |
|
unizlim |
|- ( Ord |^| { x e. On | B e. ( A ^o x ) } -> ( |^| { x e. On | B e. ( A ^o x ) } = U. |^| { x e. On | B e. ( A ^o x ) } <-> ( |^| { x e. On | B e. ( A ^o x ) } = (/) \/ Lim |^| { x e. On | B e. ( A ^o x ) } ) ) ) |
88 |
16 86 87
|
3syl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( |^| { x e. On | B e. ( A ^o x ) } = U. |^| { x e. On | B e. ( A ^o x ) } <-> ( |^| { x e. On | B e. ( A ^o x ) } = (/) \/ Lim |^| { x e. On | B e. ( A ^o x ) } ) ) ) |
89 |
85 88
|
mtbird |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> -. |^| { x e. On | B e. ( A ^o x ) } = U. |^| { x e. On | B e. ( A ^o x ) } ) |
90 |
|
orduniorsuc |
|- ( Ord |^| { x e. On | B e. ( A ^o x ) } -> ( |^| { x e. On | B e. ( A ^o x ) } = U. |^| { x e. On | B e. ( A ^o x ) } \/ |^| { x e. On | B e. ( A ^o x ) } = suc U. |^| { x e. On | B e. ( A ^o x ) } ) ) |
91 |
16 86 90
|
3syl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( |^| { x e. On | B e. ( A ^o x ) } = U. |^| { x e. On | B e. ( A ^o x ) } \/ |^| { x e. On | B e. ( A ^o x ) } = suc U. |^| { x e. On | B e. ( A ^o x ) } ) ) |
92 |
91
|
ord |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( -. |^| { x e. On | B e. ( A ^o x ) } = U. |^| { x e. On | B e. ( A ^o x ) } -> |^| { x e. On | B e. ( A ^o x ) } = suc U. |^| { x e. On | B e. ( A ^o x ) } ) ) |
93 |
89 92
|
mpd |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> |^| { x e. On | B e. ( A ^o x ) } = suc U. |^| { x e. On | B e. ( A ^o x ) } ) |
94 |
23 93
|
eqtr4id |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> suc X = |^| { x e. On | B e. ( A ^o x ) } ) |
95 |
21 94
|
eleqtrd |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> X e. |^| { x e. On | B e. ( A ^o x ) } ) |
96 |
58
|
inteqi |
|- |^| { x e. On | B e. ( A ^o x ) } = |^| { y e. On | B e. ( A ^o y ) } |
97 |
95 96
|
eleqtrdi |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> X e. |^| { y e. On | B e. ( A ^o y ) } ) |
98 |
55
|
onnminsb |
|- ( X e. On -> ( X e. |^| { y e. On | B e. ( A ^o y ) } -> -. B e. ( A ^o X ) ) ) |
99 |
19 97 98
|
sylc |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> -. B e. ( A ^o X ) ) |
100 |
|
oecl |
|- ( ( A e. On /\ X e. On ) -> ( A ^o X ) e. On ) |
101 |
39 19 100
|
syl2anc |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o X ) e. On ) |
102 |
|
ontri1 |
|- ( ( ( A ^o X ) e. On /\ B e. On ) -> ( ( A ^o X ) C_ B <-> -. B e. ( A ^o X ) ) ) |
103 |
101 3 102
|
syl2anc |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( A ^o X ) C_ B <-> -. B e. ( A ^o X ) ) ) |
104 |
99 103
|
mpbird |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( A ^o X ) C_ B ) |
105 |
94 31
|
eqeltrd |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> suc X e. { x e. On | B e. ( A ^o x ) } ) |
106 |
|
oveq2 |
|- ( y = suc X -> ( A ^o y ) = ( A ^o suc X ) ) |
107 |
106
|
eleq2d |
|- ( y = suc X -> ( B e. ( A ^o y ) <-> B e. ( A ^o suc X ) ) ) |
108 |
107 58
|
elrab2 |
|- ( suc X e. { x e. On | B e. ( A ^o x ) } <-> ( suc X e. On /\ B e. ( A ^o suc X ) ) ) |
109 |
108
|
simprbi |
|- ( suc X e. { x e. On | B e. ( A ^o x ) } -> B e. ( A ^o suc X ) ) |
110 |
105 109
|
syl |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> B e. ( A ^o suc X ) ) |
111 |
19 104 110
|
3jca |
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( X e. On /\ ( A ^o X ) C_ B /\ B e. ( A ^o suc X ) ) ) |