Metamath Proof Explorer

Theorem oeeulem

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

Ref Expression
Hypothesis oeeu.1 ⊢ 𝑋 = ∪ ∩ { 𝑥 ∈ On ∣ 𝐵 ∈ ( 𝐴 ↑o 𝑥 ) }
Assertion oeeulem ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ 𝐵 ∈ ( On ∖ 1o ) ) → ( 𝑋 ∈ On ∧ ( 𝐴 ↑o 𝑋 ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 ↑o suc 𝑋 ) ) )

Proof

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