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