Metamath Proof Explorer


Theorem oeeulem

Description: Lemma for oeeu . (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Hypothesis oeeu.1
|- X = U. |^| { x e. On | B e. ( A ^o x ) }
Assertion oeeulem
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( X e. On /\ ( A ^o X ) C_ B /\ B e. ( A ^o suc X ) ) )

Proof

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 ) ) )