| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = suc 𝐴 → (𝐶 ↑o 𝑥) = (𝐶 ↑o suc 𝐴)) | 
| 2 | 1 | eleq2d 2827 | . . . 4
⊢ (𝑥 = suc 𝐴 → ((𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥) ↔ (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝐴))) | 
| 3 | 2 | imbi2d 340 | . . 3
⊢ (𝑥 = suc 𝐴 → ((𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝐴)))) | 
| 4 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝐶 ↑o 𝑥) = (𝐶 ↑o 𝑦)) | 
| 5 | 4 | eleq2d 2827 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥) ↔ (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦))) | 
| 6 | 5 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝑦 → ((𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)))) | 
| 7 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐶 ↑o 𝑥) = (𝐶 ↑o suc 𝑦)) | 
| 8 | 7 | eleq2d 2827 | . . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥) ↔ (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝑦))) | 
| 9 | 8 | imbi2d 340 | . . 3
⊢ (𝑥 = suc 𝑦 → ((𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝑦)))) | 
| 10 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 𝐵 → (𝐶 ↑o 𝑥) = (𝐶 ↑o 𝐵)) | 
| 11 | 10 | eleq2d 2827 | . . . 4
⊢ (𝑥 = 𝐵 → ((𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥) ↔ (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵))) | 
| 12 | 11 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝐵 → ((𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥)) ↔ (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵)))) | 
| 13 |  | eldifi 4131 | . . . . . . . 8
⊢ (𝐶 ∈ (On ∖
2o) → 𝐶
∈ On) | 
| 14 |  | oecl 8575 | . . . . . . . 8
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ↑o 𝐴) ∈ On) | 
| 15 | 13, 14 | sylan 580 | . . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → (𝐶
↑o 𝐴)
∈ On) | 
| 16 |  | om1 8580 | . . . . . . 7
⊢ ((𝐶 ↑o 𝐴) ∈ On → ((𝐶 ↑o 𝐴) ·o
1o) = (𝐶
↑o 𝐴)) | 
| 17 | 15, 16 | syl 17 | . . . . . 6
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → ((𝐶
↑o 𝐴)
·o 1o) = (𝐶 ↑o 𝐴)) | 
| 18 |  | ondif2 8540 | . . . . . . . . 9
⊢ (𝐶 ∈ (On ∖
2o) ↔ (𝐶
∈ On ∧ 1o ∈ 𝐶)) | 
| 19 | 18 | simprbi 496 | . . . . . . . 8
⊢ (𝐶 ∈ (On ∖
2o) → 1o ∈ 𝐶) | 
| 20 | 19 | adantr 480 | . . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → 1o ∈ 𝐶) | 
| 21 | 13 | adantr 480 | . . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → 𝐶 ∈
On) | 
| 22 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → 𝐴 ∈
On) | 
| 23 |  | dif20el 8543 | . . . . . . . . . 10
⊢ (𝐶 ∈ (On ∖
2o) → ∅ ∈ 𝐶) | 
| 24 | 23 | adantr 480 | . . . . . . . . 9
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → ∅ ∈ 𝐶) | 
| 25 |  | oen0 8624 | . . . . . . . . 9
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐶) → ∅ ∈
(𝐶 ↑o 𝐴)) | 
| 26 | 21, 22, 24, 25 | syl21anc 838 | . . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → ∅ ∈ (𝐶 ↑o 𝐴)) | 
| 27 |  | omordi 8604 | . . . . . . . 8
⊢ (((𝐶 ∈ On ∧ (𝐶 ↑o 𝐴) ∈ On) ∧ ∅
∈ (𝐶
↑o 𝐴))
→ (1o ∈ 𝐶 → ((𝐶 ↑o 𝐴) ·o 1o) ∈
((𝐶 ↑o
𝐴) ·o
𝐶))) | 
| 28 | 21, 15, 26, 27 | syl21anc 838 | . . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → (1o ∈ 𝐶 → ((𝐶 ↑o 𝐴) ·o 1o) ∈
((𝐶 ↑o
𝐴) ·o
𝐶))) | 
| 29 | 20, 28 | mpd 15 | . . . . . 6
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → ((𝐶
↑o 𝐴)
·o 1o) ∈ ((𝐶 ↑o 𝐴) ·o 𝐶)) | 
| 30 | 17, 29 | eqeltrrd 2842 | . . . . 5
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → (𝐶
↑o 𝐴)
∈ ((𝐶
↑o 𝐴)
·o 𝐶)) | 
| 31 |  | oesuc 8565 | . . . . . 6
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ↑o suc 𝐴) = ((𝐶 ↑o 𝐴) ·o 𝐶)) | 
| 32 | 13, 31 | sylan 580 | . . . . 5
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → (𝐶
↑o suc 𝐴) =
((𝐶 ↑o
𝐴) ·o
𝐶)) | 
| 33 | 30, 32 | eleqtrrd 2844 | . . . 4
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝐴
∈ On) → (𝐶
↑o 𝐴)
∈ (𝐶
↑o suc 𝐴)) | 
| 34 | 33 | expcom 413 | . . 3
⊢ (𝐴 ∈ On → (𝐶 ∈ (On ∖
2o) → (𝐶
↑o 𝐴)
∈ (𝐶
↑o suc 𝐴))) | 
| 35 |  | oecl 8575 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ↑o 𝑦) ∈ On) | 
| 36 | 13, 35 | sylan 580 | . . . . . . . . . 10
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝐶
↑o 𝑦)
∈ On) | 
| 37 |  | om1 8580 | . . . . . . . . . 10
⊢ ((𝐶 ↑o 𝑦) ∈ On → ((𝐶 ↑o 𝑦) ·o
1o) = (𝐶
↑o 𝑦)) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . 9
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → ((𝐶
↑o 𝑦)
·o 1o) = (𝐶 ↑o 𝑦)) | 
| 39 | 19 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → 1o ∈ 𝐶) | 
| 40 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → 𝐶 ∈
On) | 
| 41 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → 𝑦 ∈
On) | 
| 42 | 23 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → ∅ ∈ 𝐶) | 
| 43 |  | oen0 8624 | . . . . . . . . . . . 12
⊢ (((𝐶 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈
𝐶) → ∅ ∈
(𝐶 ↑o 𝑦)) | 
| 44 | 40, 41, 42, 43 | syl21anc 838 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → ∅ ∈ (𝐶 ↑o 𝑦)) | 
| 45 |  | omordi 8604 | . . . . . . . . . . 11
⊢ (((𝐶 ∈ On ∧ (𝐶 ↑o 𝑦) ∈ On) ∧ ∅
∈ (𝐶
↑o 𝑦))
→ (1o ∈ 𝐶 → ((𝐶 ↑o 𝑦) ·o 1o) ∈
((𝐶 ↑o
𝑦) ·o
𝐶))) | 
| 46 | 40, 36, 44, 45 | syl21anc 838 | . . . . . . . . . 10
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (1o ∈ 𝐶 → ((𝐶 ↑o 𝑦) ·o 1o) ∈
((𝐶 ↑o
𝑦) ·o
𝐶))) | 
| 47 | 39, 46 | mpd 15 | . . . . . . . . 9
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → ((𝐶
↑o 𝑦)
·o 1o) ∈ ((𝐶 ↑o 𝑦) ·o 𝐶)) | 
| 48 | 38, 47 | eqeltrrd 2842 | . . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝐶
↑o 𝑦)
∈ ((𝐶
↑o 𝑦)
·o 𝐶)) | 
| 49 |  | oesuc 8565 | . . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ↑o suc 𝑦) = ((𝐶 ↑o 𝑦) ·o 𝐶)) | 
| 50 | 13, 49 | sylan 580 | . . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝐶
↑o suc 𝑦) =
((𝐶 ↑o
𝑦) ·o
𝐶)) | 
| 51 | 48, 50 | eleqtrrd 2844 | . . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝐶
↑o 𝑦)
∈ (𝐶
↑o suc 𝑦)) | 
| 52 |  | onsuc 7831 | . . . . . . . . 9
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) | 
| 53 |  | oecl 8575 | . . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ suc 𝑦 ∈ On) → (𝐶 ↑o suc 𝑦) ∈ On) | 
| 54 | 13, 52, 53 | syl2an 596 | . . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (𝐶
↑o suc 𝑦)
∈ On) | 
| 55 |  | ontr1 6430 | . . . . . . . 8
⊢ ((𝐶 ↑o suc 𝑦) ∈ On → (((𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦) ∧ (𝐶 ↑o 𝑦) ∈ (𝐶 ↑o suc 𝑦)) → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝑦))) | 
| 56 | 54, 55 | syl 17 | . . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → (((𝐶
↑o 𝐴)
∈ (𝐶
↑o 𝑦) ∧
(𝐶 ↑o 𝑦) ∈ (𝐶 ↑o suc 𝑦)) → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝑦))) | 
| 57 | 51, 56 | mpan2d 694 | . . . . . 6
⊢ ((𝐶 ∈ (On ∖
2o) ∧ 𝑦
∈ On) → ((𝐶
↑o 𝐴)
∈ (𝐶
↑o 𝑦)
→ (𝐶
↑o 𝐴)
∈ (𝐶
↑o suc 𝑦))) | 
| 58 | 57 | expcom 413 | . . . . 5
⊢ (𝑦 ∈ On → (𝐶 ∈ (On ∖
2o) → ((𝐶
↑o 𝐴)
∈ (𝐶
↑o 𝑦)
→ (𝐶
↑o 𝐴)
∈ (𝐶
↑o suc 𝑦)))) | 
| 59 | 58 | adantr 480 | . . . 4
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ 𝑦) → (𝐶 ∈ (On ∖ 2o) →
((𝐶 ↑o
𝐴) ∈ (𝐶 ↑o 𝑦) → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝑦)))) | 
| 60 | 59 | a2d 29 | . . 3
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ 𝑦) → ((𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝑦)))) | 
| 61 |  | bi2.04 387 | . . . . . 6
⊢ ((𝐴 ∈ 𝑦 → (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) →
(𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)))) | 
| 62 | 61 | ralbii 3093 | . . . . 5
⊢
(∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦))) ↔ ∀𝑦 ∈ 𝑥 (𝐶 ∈ (On ∖ 2o) →
(𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)))) | 
| 63 |  | r19.21v 3180 | . . . . 5
⊢
(∀𝑦 ∈
𝑥 (𝐶 ∈ (On ∖ 2o) →
(𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) →
∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)))) | 
| 64 | 62, 63 | bitri 275 | . . . 4
⊢
(∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦))) ↔ (𝐶 ∈ (On ∖ 2o) →
∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)))) | 
| 65 |  | limsuc 7870 | . . . . . . . . . 10
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥)) | 
| 66 | 65 | biimpa 476 | . . . . . . . . 9
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → suc 𝐴 ∈ 𝑥) | 
| 67 |  | elex 3501 | . . . . . . . . . . . . 13
⊢ (suc
𝐴 ∈ 𝑥 → suc 𝐴 ∈ V) | 
| 68 |  | sucexb 7824 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) | 
| 69 |  | sucidg 6465 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) | 
| 70 | 68, 69 | sylbir 235 | . . . . . . . . . . . . 13
⊢ (suc
𝐴 ∈ V → 𝐴 ∈ suc 𝐴) | 
| 71 | 67, 70 | syl 17 | . . . . . . . . . . . 12
⊢ (suc
𝐴 ∈ 𝑥 → 𝐴 ∈ suc 𝐴) | 
| 72 |  | eleq2 2830 | . . . . . . . . . . . . . 14
⊢ (𝑦 = suc 𝐴 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ suc 𝐴)) | 
| 73 |  | oveq2 7439 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = suc 𝐴 → (𝐶 ↑o 𝑦) = (𝐶 ↑o suc 𝐴)) | 
| 74 | 73 | eleq2d 2827 | . . . . . . . . . . . . . 14
⊢ (𝑦 = suc 𝐴 → ((𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦) ↔ (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝐴))) | 
| 75 | 72, 74 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑦 = suc 𝐴 → ((𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) ↔ (𝐴 ∈ suc 𝐴 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝐴)))) | 
| 76 | 75 | rspcv 3618 | . . . . . . . . . . . 12
⊢ (suc
𝐴 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (𝐴 ∈ suc 𝐴 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝐴)))) | 
| 77 | 71, 76 | mpid 44 | . . . . . . . . . . 11
⊢ (suc
𝐴 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝐴))) | 
| 78 | 77 | anc2li 555 | . . . . . . . . . 10
⊢ (suc
𝐴 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (suc 𝐴 ∈ 𝑥 ∧ (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝐴)))) | 
| 79 | 73 | eliuni 4997 | . . . . . . . . . 10
⊢ ((suc
𝐴 ∈ 𝑥 ∧ (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o suc 𝐴)) → (𝐶 ↑o 𝐴) ∈ ∪
𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦)) | 
| 80 | 78, 79 | syl6 35 | . . . . . . . . 9
⊢ (suc
𝐴 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (𝐶 ↑o 𝐴) ∈ ∪
𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦))) | 
| 81 | 66, 80 | syl 17 | . . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (𝐶 ↑o 𝐴) ∈ ∪
𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦))) | 
| 82 | 81 | adantr 480 | . . . . . . 7
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) →
(∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (𝐶 ↑o 𝐴) ∈ ∪
𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦))) | 
| 83 | 13 | adantl 481 | . . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ (On ∖ 2o)) →
𝐶 ∈
On) | 
| 84 |  | simpl 482 | . . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ (On ∖ 2o)) →
Lim 𝑥) | 
| 85 | 23 | adantl 481 | . . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ (On ∖ 2o)) →
∅ ∈ 𝐶) | 
| 86 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑥 ∈ V | 
| 87 |  | oelim 8572 | . . . . . . . . . . 11
⊢ (((𝐶 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐶) → (𝐶 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦)) | 
| 88 | 86, 87 | mpanlr1 706 | . . . . . . . . . 10
⊢ (((𝐶 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐶) → (𝐶 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦)) | 
| 89 | 83, 84, 85, 88 | syl21anc 838 | . . . . . . . . 9
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ (On ∖ 2o)) →
(𝐶 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦)) | 
| 90 | 89 | adantlr 715 | . . . . . . . 8
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) →
(𝐶 ↑o 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦)) | 
| 91 | 90 | eleq2d 2827 | . . . . . . 7
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) →
((𝐶 ↑o
𝐴) ∈ (𝐶 ↑o 𝑥) ↔ (𝐶 ↑o 𝐴) ∈ ∪
𝑦 ∈ 𝑥 (𝐶 ↑o 𝑦))) | 
| 92 | 82, 91 | sylibrd 259 | . . . . . 6
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) ∧ 𝐶 ∈ (On ∖ 2o)) →
(∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥))) | 
| 93 | 92 | ex 412 | . . . . 5
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → (𝐶 ∈ (On ∖ 2o) →
(∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦)) → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥)))) | 
| 94 | 93 | a2d 29 | . . . 4
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → ((𝐶 ∈ (On ∖ 2o) →
∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦))) → (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥)))) | 
| 95 | 64, 94 | biimtrid 242 | . . 3
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑦))) → (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝑥)))) | 
| 96 | 3, 6, 9, 12, 34, 60, 95 | tfindsg2 7883 | . 2
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐶 ∈ (On ∖ 2o) →
(𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵))) | 
| 97 | 96 | impancom 451 | 1
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐴
∈ 𝐵 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵))) |