| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | naddwordnexlem4.s | . . . . 5
⊢ 𝑆 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} | 
| 2 | 1 | ssrab3 4081 | . . . 4
⊢ 𝑆 ⊆ On | 
| 3 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑦 = 𝐷 → (𝐶 +o 𝑦) = (𝐶 +o 𝐷)) | 
| 4 | 3 | sseq2d 4015 | . . . . . . 7
⊢ (𝑦 = 𝐷 → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o 𝐷))) | 
| 5 |  | naddwordnex.d | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ On) | 
| 6 |  | naddwordnex.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝐷) | 
| 7 |  | onelon 6408 | . . . . . . . . 9
⊢ ((𝐷 ∈ On ∧ 𝐶 ∈ 𝐷) → 𝐶 ∈ On) | 
| 8 | 5, 6, 7 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ On) | 
| 9 |  | oaword2 8592 | . . . . . . . 8
⊢ ((𝐷 ∈ On ∧ 𝐶 ∈ On) → 𝐷 ⊆ (𝐶 +o 𝐷)) | 
| 10 | 5, 8, 9 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ (𝐶 +o 𝐷)) | 
| 11 | 4, 5, 10 | elrabd 3693 | . . . . . 6
⊢ (𝜑 → 𝐷 ∈ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}) | 
| 12 | 11, 1 | eleqtrrdi 2851 | . . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑆) | 
| 13 | 12 | ne0d 4341 | . . . 4
⊢ (𝜑 → 𝑆 ≠ ∅) | 
| 14 |  | oninton 7816 | . . . 4
⊢ ((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ On) | 
| 15 | 2, 13, 14 | sylancr 587 | . . 3
⊢ (𝜑 → ∩ 𝑆
∈ On) | 
| 16 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → (𝐶 +o 𝑦) = (𝐶 +o ∅)) | 
| 17 |  | oa0 8555 | . . . . . . . . . . . . . 14
⊢ (𝐶 ∈ On → (𝐶 +o ∅) = 𝐶) | 
| 18 | 8, 17 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 +o ∅) = 𝐶) | 
| 19 | 16, 18 | sylan9eqr 2798 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐶 +o 𝑦) = 𝐶) | 
| 20 | 6 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝐶 ∈ 𝐷) | 
| 21 | 19, 20 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐶 +o 𝑦) ∈ 𝐷) | 
| 22 | 21 | ex 412 | . . . . . . . . . 10
⊢ (𝜑 → (𝑦 = ∅ → (𝐶 +o 𝑦) ∈ 𝐷)) | 
| 23 | 22 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝑦 = ∅ → (𝐶 +o 𝑦) ∈ 𝐷)) | 
| 24 | 23 | con3d 152 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (¬ (𝐶 +o 𝑦) ∈ 𝐷 → ¬ 𝑦 = ∅)) | 
| 25 |  | oacl 8574 | . . . . . . . . . 10
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 +o 𝑦) ∈ On) | 
| 26 | 8, 25 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐶 +o 𝑦) ∈ On) | 
| 27 |  | ontri1 6417 | . . . . . . . . 9
⊢ ((𝐷 ∈ On ∧ (𝐶 +o 𝑦) ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ ¬ (𝐶 +o 𝑦) ∈ 𝐷)) | 
| 28 | 5, 26, 27 | syl2an2r 685 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ ¬ (𝐶 +o 𝑦) ∈ 𝐷)) | 
| 29 |  | on0eln0 6439 | . . . . . . . . . 10
⊢ (𝑦 ∈ On → (∅
∈ 𝑦 ↔ 𝑦 ≠ ∅)) | 
| 30 |  | df-ne 2940 | . . . . . . . . . 10
⊢ (𝑦 ≠ ∅ ↔ ¬ 𝑦 = ∅) | 
| 31 | 29, 30 | bitrdi 287 | . . . . . . . . 9
⊢ (𝑦 ∈ On → (∅
∈ 𝑦 ↔ ¬ 𝑦 = ∅)) | 
| 32 | 31 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (∅ ∈ 𝑦 ↔ ¬ 𝑦 = ∅)) | 
| 33 | 24, 28, 32 | 3imtr4d 294 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦)) | 
| 34 | 33 | ex 412 | . . . . . 6
⊢ (𝜑 → (𝑦 ∈ On → (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦))) | 
| 35 | 34 | ralrimiv 3144 | . . . . 5
⊢ (𝜑 → ∀𝑦 ∈ On (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦)) | 
| 36 |  | 0ex 5306 | . . . . . 6
⊢ ∅
∈ V | 
| 37 | 36 | elintrab 4959 | . . . . 5
⊢ (∅
∈ ∩ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} ↔ ∀𝑦 ∈ On (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦)) | 
| 38 | 35, 37 | sylibr 234 | . . . 4
⊢ (𝜑 → ∅ ∈ ∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)}) | 
| 39 | 1 | inteqi 4949 | . . . 4
⊢ ∩ 𝑆 =
∩ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} | 
| 40 | 38, 39 | eleqtrrdi 2851 | . . 3
⊢ (𝜑 → ∅ ∈ ∩ 𝑆) | 
| 41 |  | ondif1 8540 | . . 3
⊢ (∩ 𝑆
∈ (On ∖ 1o) ↔ (∩ 𝑆 ∈ On ∧ ∅ ∈
∩ 𝑆)) | 
| 42 | 15, 40, 41 | sylanbrc 583 | . 2
⊢ (𝜑 → ∩ 𝑆
∈ (On ∖ 1o)) | 
| 43 |  | onzsl 7868 | . . . . . 6
⊢ (∩ 𝑆
∈ On ↔ (∩ 𝑆 = ∅ ∨ ∃𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆))) | 
| 44 | 15, 43 | sylib 218 | . . . . 5
⊢ (𝜑 → (∩ 𝑆 =
∅ ∨ ∃𝑧
∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆))) | 
| 45 |  | oveq2 7440 | . . . . . . . . 9
⊢ (∩ 𝑆 =
∅ → (𝐶
+o ∩ 𝑆) = (𝐶 +o ∅)) | 
| 46 | 45, 18 | sylan9eqr 2798 | . . . . . . . 8
⊢ ((𝜑 ∧ ∩ 𝑆 =
∅) → (𝐶
+o ∩ 𝑆) = 𝐶) | 
| 47 |  | onelpss 6423 | . . . . . . . . . . . 12
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → (𝐶 ∈ 𝐷 ↔ (𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷))) | 
| 48 | 8, 5, 47 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶 ∈ 𝐷 ↔ (𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷))) | 
| 49 | 6, 48 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷)) | 
| 50 | 49 | simpld 494 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ⊆ 𝐷) | 
| 51 | 50 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ∩ 𝑆 =
∅) → 𝐶 ⊆
𝐷) | 
| 52 | 46, 51 | eqsstrd 4017 | . . . . . . 7
⊢ ((𝜑 ∧ ∩ 𝑆 =
∅) → (𝐶
+o ∩ 𝑆) ⊆ 𝐷) | 
| 53 | 52 | ex 412 | . . . . . 6
⊢ (𝜑 → (∩ 𝑆 =
∅ → (𝐶
+o ∩ 𝑆) ⊆ 𝐷)) | 
| 54 |  | oveq2 7440 | . . . . . . . . 9
⊢ (∩ 𝑆 =
suc 𝑧 → (𝐶 +o ∩ 𝑆) =
(𝐶 +o suc 𝑧)) | 
| 55 |  | oasuc 8563 | . . . . . . . . . 10
⊢ ((𝐶 ∈ On ∧ 𝑧 ∈ On) → (𝐶 +o suc 𝑧) = suc (𝐶 +o 𝑧)) | 
| 56 | 8, 55 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝐶 +o suc 𝑧) = suc (𝐶 +o 𝑧)) | 
| 57 | 54, 56 | sylan9eqr 2798 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ ∩ 𝑆 =
suc 𝑧) → (𝐶 +o ∩ 𝑆) =
suc (𝐶 +o 𝑧)) | 
| 58 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑧 ∈ V | 
| 59 | 58 | sucid 6465 | . . . . . . . . . . . 12
⊢ 𝑧 ∈ suc 𝑧 | 
| 60 |  | eleq2 2829 | . . . . . . . . . . . 12
⊢ (∩ 𝑆 =
suc 𝑧 → (𝑧 ∈ ∩ 𝑆
↔ 𝑧 ∈ suc 𝑧)) | 
| 61 | 59, 60 | mpbiri 258 | . . . . . . . . . . 11
⊢ (∩ 𝑆 =
suc 𝑧 → 𝑧 ∈ ∩ 𝑆) | 
| 62 | 61 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∩ 𝑆 =
suc 𝑧 → 𝑧 ∈ ∩ 𝑆)) | 
| 63 | 39 | eleq2i 2832 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ∩ 𝑆
↔ 𝑧 ∈ ∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)}) | 
| 64 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝐶 +o 𝑦) = (𝐶 +o 𝑧)) | 
| 65 | 64 | sseq2d 4015 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o 𝑧))) | 
| 66 | 65 | onnminsb 7820 | . . . . . . . . . . . . 13
⊢ (𝑧 ∈ On → (𝑧 ∈ ∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)} → ¬ 𝐷 ⊆ (𝐶 +o 𝑧))) | 
| 67 | 66 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝑧 ∈ ∩ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → ¬ 𝐷 ⊆ (𝐶 +o 𝑧))) | 
| 68 | 63, 67 | biimtrid 242 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝑧 ∈ ∩ 𝑆 → ¬ 𝐷 ⊆ (𝐶 +o 𝑧))) | 
| 69 |  | oacl 8574 | . . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ On ∧ 𝑧 ∈ On) → (𝐶 +o 𝑧) ∈ On) | 
| 70 | 8, 69 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝐶 +o 𝑧) ∈ On) | 
| 71 |  | ontri1 6417 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∈ On ∧ (𝐶 +o 𝑧) ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑧) ↔ ¬ (𝐶 +o 𝑧) ∈ 𝐷)) | 
| 72 | 5, 70, 71 | syl2an2r 685 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑧) ↔ ¬ (𝐶 +o 𝑧) ∈ 𝐷)) | 
| 73 | 72 | con2bid 354 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ On) → ((𝐶 +o 𝑧) ∈ 𝐷 ↔ ¬ 𝐷 ⊆ (𝐶 +o 𝑧))) | 
| 74 | 68, 73 | sylibrd 259 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝑧 ∈ ∩ 𝑆 → (𝐶 +o 𝑧) ∈ 𝐷)) | 
| 75 |  | onsucss 43284 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ On → ((𝐶 +o 𝑧) ∈ 𝐷 → suc (𝐶 +o 𝑧) ⊆ 𝐷)) | 
| 76 | 5, 75 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 +o 𝑧) ∈ 𝐷 → suc (𝐶 +o 𝑧) ⊆ 𝐷)) | 
| 77 | 76 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ On) → ((𝐶 +o 𝑧) ∈ 𝐷 → suc (𝐶 +o 𝑧) ⊆ 𝐷)) | 
| 78 | 62, 74, 77 | 3syld 60 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∩ 𝑆 =
suc 𝑧 → suc (𝐶 +o 𝑧) ⊆ 𝐷)) | 
| 79 | 78 | imp 406 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ ∩ 𝑆 =
suc 𝑧) → suc (𝐶 +o 𝑧) ⊆ 𝐷) | 
| 80 | 57, 79 | eqsstrd 4017 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ ∩ 𝑆 =
suc 𝑧) → (𝐶 +o ∩ 𝑆)
⊆ 𝐷) | 
| 81 | 80 | rexlimdva2 3156 | . . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ On ∩ 𝑆 = suc 𝑧 → (𝐶 +o ∩
𝑆) ⊆ 𝐷)) | 
| 82 |  | oalim 8571 | . . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → (𝐶 +o ∩
𝑆) = ∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧)) | 
| 83 | 8, 82 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → (𝐶 +o ∩
𝑆) = ∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧)) | 
| 84 |  | onelon 6408 | . . . . . . . . . . . . . . 15
⊢ ((∩ 𝑆
∈ On ∧ 𝑧 ∈
∩ 𝑆) → 𝑧 ∈ On) | 
| 85 | 15, 84 | sylan 580 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ ∩ 𝑆) → 𝑧 ∈ On) | 
| 86 | 85 | ex 412 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑧 ∈ ∩ 𝑆 → 𝑧 ∈ On)) | 
| 87 | 86 | ancrd 551 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ ∩ 𝑆 → (𝑧 ∈ On ∧ 𝑧 ∈ ∩ 𝑆))) | 
| 88 | 74 | expimpd 453 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑧 ∈ On ∧ 𝑧 ∈ ∩ 𝑆) → (𝐶 +o 𝑧) ∈ 𝐷)) | 
| 89 |  | onelss 6425 | . . . . . . . . . . . . 13
⊢ (𝐷 ∈ On → ((𝐶 +o 𝑧) ∈ 𝐷 → (𝐶 +o 𝑧) ⊆ 𝐷)) | 
| 90 | 5, 89 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 +o 𝑧) ∈ 𝐷 → (𝐶 +o 𝑧) ⊆ 𝐷)) | 
| 91 | 87, 88, 90 | 3syld 60 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ ∩ 𝑆 → (𝐶 +o 𝑧) ⊆ 𝐷)) | 
| 92 | 91 | ralrimiv 3144 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷) | 
| 93 |  | iunss 5044 | . . . . . . . . . 10
⊢ (∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷 ↔ ∀𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷) | 
| 94 | 92, 93 | sylibr 234 | . . . . . . . . 9
⊢ (𝜑 → ∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷) | 
| 95 | 94 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → ∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷) | 
| 96 | 83, 95 | eqsstrd 4017 | . . . . . . 7
⊢ ((𝜑 ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → (𝐶 +o ∩
𝑆) ⊆ 𝐷) | 
| 97 | 96 | ex 412 | . . . . . 6
⊢ (𝜑 → ((∩ 𝑆
∈ V ∧ Lim ∩ 𝑆) → (𝐶 +o ∩
𝑆) ⊆ 𝐷)) | 
| 98 | 53, 81, 97 | 3jaod 1430 | . . . . 5
⊢ (𝜑 → ((∩ 𝑆 =
∅ ∨ ∃𝑧
∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆))
→ (𝐶 +o
∩ 𝑆) ⊆ 𝐷)) | 
| 99 | 44, 98 | mpd 15 | . . . 4
⊢ (𝜑 → (𝐶 +o ∩
𝑆) ⊆ 𝐷) | 
| 100 | 4 | rspcev 3621 | . . . . . . 7
⊢ ((𝐷 ∈ On ∧ 𝐷 ⊆ (𝐶 +o 𝐷)) → ∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦)) | 
| 101 | 5, 10, 100 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦)) | 
| 102 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑦𝐷 | 
| 103 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑦𝐶 | 
| 104 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑦
+o | 
| 105 |  | nfrab1 3456 | . . . . . . . . . 10
⊢
Ⅎ𝑦{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} | 
| 106 | 105 | nfint 4955 | . . . . . . . . 9
⊢
Ⅎ𝑦∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)} | 
| 107 | 103, 104,
106 | nfov 7462 | . . . . . . . 8
⊢
Ⅎ𝑦(𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}) | 
| 108 | 102, 107 | nfss 3975 | . . . . . . 7
⊢
Ⅎ𝑦 𝐷 ⊆ (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}) | 
| 109 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → (𝐶 +o 𝑦) = (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})) | 
| 110 | 109 | sseq2d 4015 | . . . . . . 7
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}))) | 
| 111 | 108, 110 | onminsb 7815 | . . . . . 6
⊢
(∃𝑦 ∈ On
𝐷 ⊆ (𝐶 +o 𝑦) → 𝐷 ⊆ (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})) | 
| 112 | 101, 111 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐷 ⊆ (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})) | 
| 113 | 39 | oveq2i 7443 | . . . . 5
⊢ (𝐶 +o ∩ 𝑆) =
(𝐶 +o ∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)}) | 
| 114 | 112, 113 | sseqtrrdi 4024 | . . . 4
⊢ (𝜑 → 𝐷 ⊆ (𝐶 +o ∩
𝑆)) | 
| 115 | 99, 114 | eqssd 4000 | . . 3
⊢ (𝜑 → (𝐶 +o ∩
𝑆) = 𝐷) | 
| 116 |  | omelon 9687 | . . . . . 6
⊢ ω
∈ On | 
| 117 |  | omcl 8575 | . . . . . 6
⊢ ((ω
∈ On ∧ 𝐷 ∈
On) → (ω ·o 𝐷) ∈ On) | 
| 118 | 116, 5, 117 | sylancr 587 | . . . . 5
⊢ (𝜑 → (ω
·o 𝐷)
∈ On) | 
| 119 | 116 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ω ∈
On) | 
| 120 |  | naddwordnex.n | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ 𝑀) | 
| 121 |  | naddwordnex.m | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ω) | 
| 122 | 120, 121 | jca 511 | . . . . . . 7
⊢ (𝜑 → (𝑁 ∈ 𝑀 ∧ 𝑀 ∈ ω)) | 
| 123 |  | ontr1 6429 | . . . . . . 7
⊢ (ω
∈ On → ((𝑁 ∈
𝑀 ∧ 𝑀 ∈ ω) → 𝑁 ∈ ω)) | 
| 124 | 119, 122,
123 | sylc 65 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ω) | 
| 125 |  | nnon 7894 | . . . . . 6
⊢ (𝑁 ∈ ω → 𝑁 ∈ On) | 
| 126 | 124, 125 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ On) | 
| 127 |  | oaword1 8591 | . . . . 5
⊢
(((ω ·o 𝐷) ∈ On ∧ 𝑁 ∈ On) → (ω
·o 𝐷)
⊆ ((ω ·o 𝐷) +o 𝑁)) | 
| 128 | 118, 126,
127 | syl2anc 584 | . . . 4
⊢ (𝜑 → (ω
·o 𝐷)
⊆ ((ω ·o 𝐷) +o 𝑁)) | 
| 129 |  | naddwordnex.a | . . . . . 6
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) | 
| 130 | 129 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → (𝐴 +o (ω ·o
∩ 𝑆)) = (((ω ·o 𝐶) +o 𝑀) +o (ω
·o ∩ 𝑆))) | 
| 131 |  | omcl 8575 | . . . . . . 7
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ·o 𝐶) ∈ On) | 
| 132 | 116, 8, 131 | sylancr 587 | . . . . . 6
⊢ (𝜑 → (ω
·o 𝐶)
∈ On) | 
| 133 |  | nnon 7894 | . . . . . . 7
⊢ (𝑀 ∈ ω → 𝑀 ∈ On) | 
| 134 | 121, 133 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ On) | 
| 135 |  | omcl 8575 | . . . . . . 7
⊢ ((ω
∈ On ∧ ∩ 𝑆 ∈ On) → (ω
·o ∩ 𝑆) ∈ On) | 
| 136 | 116, 15, 135 | sylancr 587 | . . . . . 6
⊢ (𝜑 → (ω
·o ∩ 𝑆) ∈ On) | 
| 137 |  | oaass 8600 | . . . . . 6
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → (((ω
·o 𝐶)
+o 𝑀)
+o (ω ·o ∩ 𝑆)) = ((ω
·o 𝐶)
+o (𝑀
+o (ω ·o ∩ 𝑆)))) | 
| 138 | 132, 134,
136, 137 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (((ω
·o 𝐶)
+o 𝑀)
+o (ω ·o ∩ 𝑆)) = ((ω
·o 𝐶)
+o (𝑀
+o (ω ·o ∩ 𝑆)))) | 
| 139 | 15, 116 | jctil 519 | . . . . . . . . 9
⊢ (𝜑 → (ω ∈ On ∧
∩ 𝑆 ∈ On)) | 
| 140 |  | omword1 8612 | . . . . . . . . 9
⊢
(((ω ∈ On ∧ ∩ 𝑆 ∈ On) ∧ ∅ ∈
∩ 𝑆) → ω ⊆ (ω
·o ∩ 𝑆)) | 
| 141 | 139, 40, 140 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → ω ⊆ (ω
·o ∩ 𝑆)) | 
| 142 |  | oaabs 8687 | . . . . . . . 8
⊢ (((𝑀 ∈ ω ∧ (ω
·o ∩ 𝑆) ∈ On) ∧ ω ⊆ (ω
·o ∩ 𝑆)) → (𝑀 +o (ω ·o
∩ 𝑆)) = (ω ·o ∩ 𝑆)) | 
| 143 | 121, 136,
141, 142 | syl21anc 837 | . . . . . . 7
⊢ (𝜑 → (𝑀 +o (ω ·o
∩ 𝑆)) = (ω ·o ∩ 𝑆)) | 
| 144 | 143 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → ((ω
·o 𝐶)
+o (𝑀
+o (ω ·o ∩ 𝑆))) = ((ω
·o 𝐶)
+o (ω ·o ∩ 𝑆))) | 
| 145 |  | odi 8618 | . . . . . . 7
⊢ ((ω
∈ On ∧ 𝐶 ∈ On
∧ ∩ 𝑆 ∈ On) → (ω
·o (𝐶
+o ∩ 𝑆)) = ((ω ·o 𝐶) +o (ω
·o ∩ 𝑆))) | 
| 146 | 119, 8, 15, 145 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (ω
·o (𝐶
+o ∩ 𝑆)) = ((ω ·o 𝐶) +o (ω
·o ∩ 𝑆))) | 
| 147 | 115 | oveq2d 7448 | . . . . . 6
⊢ (𝜑 → (ω
·o (𝐶
+o ∩ 𝑆)) = (ω ·o 𝐷)) | 
| 148 | 144, 146,
147 | 3eqtr2d 2782 | . . . . 5
⊢ (𝜑 → ((ω
·o 𝐶)
+o (𝑀
+o (ω ·o ∩ 𝑆))) = (ω
·o 𝐷)) | 
| 149 | 130, 138,
148 | 3eqtrd 2780 | . . . 4
⊢ (𝜑 → (𝐴 +o (ω ·o
∩ 𝑆)) = (ω ·o 𝐷)) | 
| 150 |  | naddwordnex.b | . . . 4
⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) | 
| 151 | 128, 149,
150 | 3sstr4d 4038 | . . 3
⊢ (𝜑 → (𝐴 +o (ω ·o
∩ 𝑆)) ⊆ 𝐵) | 
| 152 |  | naddcl 8716 | . . . . . . . 8
⊢
(((ω ·o 𝐶) ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) ∈ On) | 
| 153 | 132, 136,
152 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) ∈ On) | 
| 154 | 118, 153,
134 | 3jca 1128 | . . . . . 6
⊢ (𝜑 → ((ω
·o 𝐷)
∈ On ∧ ((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
∈ On ∧ 𝑀 ∈
On)) | 
| 155 | 147, 146 | eqtr3d 2778 | . . . . . . 7
⊢ (𝜑 → (ω
·o 𝐷) =
((ω ·o 𝐶) +o (ω
·o ∩ 𝑆))) | 
| 156 |  | naddgeoa 43412 | . . . . . . . 8
⊢
(((ω ·o 𝐶) ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → ((ω
·o 𝐶)
+o (ω ·o ∩ 𝑆)) ⊆ ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆))) | 
| 157 | 132, 136,
156 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((ω
·o 𝐶)
+o (ω ·o ∩ 𝑆)) ⊆ ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆))) | 
| 158 | 155, 157 | eqsstrd 4017 | . . . . . 6
⊢ (𝜑 → (ω
·o 𝐷)
⊆ ((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))) | 
| 159 |  | oawordri 8589 | . . . . . 6
⊢
(((ω ·o 𝐷) ∈ On ∧ ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) ∈ On ∧ 𝑀 ∈ On) → ((ω
·o 𝐷)
⊆ ((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
→ ((ω ·o 𝐷) +o 𝑀) ⊆ (((ω ·o
𝐶) +no (ω
·o ∩ 𝑆)) +o 𝑀))) | 
| 160 | 154, 158,
159 | sylc 65 | . . . . 5
⊢ (𝜑 → ((ω
·o 𝐷)
+o 𝑀) ⊆
(((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
+o 𝑀)) | 
| 161 |  | naddonnn 43413 | . . . . . . . . 9
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ ω) → ((ω
·o 𝐶)
+o 𝑀) =
((ω ·o 𝐶) +no 𝑀)) | 
| 162 | 132, 121,
161 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → ((ω
·o 𝐶)
+o 𝑀) =
((ω ·o 𝐶) +no 𝑀)) | 
| 163 | 129, 162 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +no 𝑀)) | 
| 164 | 163 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → (𝐴 +no (ω ·o ∩ 𝑆))
= (((ω ·o 𝐶) +no 𝑀) +no (ω ·o ∩ 𝑆))) | 
| 165 |  | naddass 8735 | . . . . . . . 8
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → (((ω
·o 𝐶) +no
𝑀) +no (ω
·o ∩ 𝑆)) = ((ω ·o 𝐶) +no (𝑀 +no (ω ·o ∩ 𝑆)))) | 
| 166 | 132, 134,
136, 165 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → (((ω
·o 𝐶) +no
𝑀) +no (ω
·o ∩ 𝑆)) = ((ω ·o 𝐶) +no (𝑀 +no (ω ·o ∩ 𝑆)))) | 
| 167 |  | naddcom 8721 | . . . . . . . . 9
⊢ ((𝑀 ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → (𝑀 +no (ω ·o ∩ 𝑆))
= ((ω ·o ∩ 𝑆) +no 𝑀)) | 
| 168 | 134, 136,
167 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑀 +no (ω ·o ∩ 𝑆))
= ((ω ·o ∩ 𝑆) +no 𝑀)) | 
| 169 | 168 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → ((ω
·o 𝐶) +no
(𝑀 +no (ω
·o ∩ 𝑆))) = ((ω ·o 𝐶) +no ((ω
·o ∩ 𝑆) +no 𝑀))) | 
| 170 |  | naddonnn 43413 | . . . . . . . . 9
⊢
((((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
∈ On ∧ 𝑀 ∈
ω) → (((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
+o 𝑀) =
(((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
+no 𝑀)) | 
| 171 | 153, 121,
170 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) +o 𝑀) = (((ω ·o 𝐶) +no (ω
·o ∩ 𝑆)) +no 𝑀)) | 
| 172 |  | naddass 8735 | . . . . . . . . 9
⊢
(((ω ·o 𝐶) ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On ∧ 𝑀 ∈ On) → (((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) +no 𝑀) = ((ω ·o 𝐶) +no ((ω
·o ∩ 𝑆) +no 𝑀))) | 
| 173 | 132, 136,
134, 172 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) +no 𝑀) = ((ω ·o 𝐶) +no ((ω
·o ∩ 𝑆) +no 𝑀))) | 
| 174 | 171, 173 | eqtr2d 2777 | . . . . . . 7
⊢ (𝜑 → ((ω
·o 𝐶) +no
((ω ·o ∩ 𝑆) +no 𝑀)) = (((ω ·o 𝐶) +no (ω
·o ∩ 𝑆)) +o 𝑀)) | 
| 175 | 166, 169,
174 | 3eqtrd 2780 | . . . . . 6
⊢ (𝜑 → (((ω
·o 𝐶) +no
𝑀) +no (ω
·o ∩ 𝑆)) = (((ω ·o 𝐶) +no (ω
·o ∩ 𝑆)) +o 𝑀)) | 
| 176 | 164, 175 | eqtr2d 2777 | . . . . 5
⊢ (𝜑 → (((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) +o 𝑀) = (𝐴 +no (ω ·o ∩ 𝑆))) | 
| 177 | 160, 176 | sseqtrd 4019 | . . . 4
⊢ (𝜑 → ((ω
·o 𝐷)
+o 𝑀) ⊆
(𝐴 +no (ω
·o ∩ 𝑆))) | 
| 178 | 134, 118 | jca 511 | . . . . . 6
⊢ (𝜑 → (𝑀 ∈ On ∧ (ω
·o 𝐷)
∈ On)) | 
| 179 |  | oaordi 8585 | . . . . . 6
⊢ ((𝑀 ∈ On ∧ (ω
·o 𝐷)
∈ On) → (𝑁 ∈
𝑀 → ((ω
·o 𝐷)
+o 𝑁) ∈
((ω ·o 𝐷) +o 𝑀))) | 
| 180 | 178, 120,
179 | sylc 65 | . . . . 5
⊢ (𝜑 → ((ω
·o 𝐷)
+o 𝑁) ∈
((ω ·o 𝐷) +o 𝑀)) | 
| 181 | 150, 180 | eqeltrd 2840 | . . . 4
⊢ (𝜑 → 𝐵 ∈ ((ω ·o 𝐷) +o 𝑀)) | 
| 182 | 177, 181 | sseldd 3983 | . . 3
⊢ (𝜑 → 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆))) | 
| 183 | 115, 151,
182 | 3jca 1128 | . 2
⊢ (𝜑 → ((𝐶 +o ∩
𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o
∩ 𝑆)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆)))) | 
| 184 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = ∩
𝑆 → (𝐶 +o 𝑥) = (𝐶 +o ∩
𝑆)) | 
| 185 | 184 | eqeq1d 2738 | . . . 4
⊢ (𝑥 = ∩
𝑆 → ((𝐶 +o 𝑥) = 𝐷 ↔ (𝐶 +o ∩
𝑆) = 𝐷)) | 
| 186 |  | oveq2 7440 | . . . . . 6
⊢ (𝑥 = ∩
𝑆 → (ω
·o 𝑥) =
(ω ·o ∩ 𝑆)) | 
| 187 | 186 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = ∩
𝑆 → (𝐴 +o (ω ·o
𝑥)) = (𝐴 +o (ω ·o
∩ 𝑆))) | 
| 188 | 187 | sseq1d 4014 | . . . 4
⊢ (𝑥 = ∩
𝑆 → ((𝐴 +o (ω
·o 𝑥))
⊆ 𝐵 ↔ (𝐴 +o (ω
·o ∩ 𝑆)) ⊆ 𝐵)) | 
| 189 | 186 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = ∩
𝑆 → (𝐴 +no (ω ·o 𝑥)) = (𝐴 +no (ω ·o ∩ 𝑆))) | 
| 190 | 189 | eleq2d 2826 | . . . 4
⊢ (𝑥 = ∩
𝑆 → (𝐵 ∈ (𝐴 +no (ω ·o 𝑥)) ↔ 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆)))) | 
| 191 | 185, 188,
190 | 3anbi123d 1437 | . . 3
⊢ (𝑥 = ∩
𝑆 → (((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o
𝑥)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o 𝑥))) ↔ ((𝐶 +o ∩
𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o
∩ 𝑆)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆))))) | 
| 192 | 191 | rspcev 3621 | . 2
⊢ ((∩ 𝑆
∈ (On ∖ 1o) ∧ ((𝐶 +o ∩
𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o
∩ 𝑆)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆)))) → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o
𝑥)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o 𝑥)))) | 
| 193 | 42, 183, 192 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o
𝑥)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o 𝑥)))) |