Metamath Proof Explorer

Theorem oeeulem

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

Ref Expression
Hypothesis oeeu.1 ⊢X=⋃⋂x∈On|B∈A↑𝑜x
Assertion oeeulem ⊢A∈On∖2𝑜∧B∈On∖1𝑜→X∈On∧A↑𝑜X⊆B∧B∈A↑𝑜suc⁡X

Proof

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