Step | Hyp | Ref
| Expression |
1 | | naddwordnexlem4.s |
. . . . 5
⊢ 𝑆 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} |
2 | 1 | ssrab3 4072 |
. . . 4
⊢ 𝑆 ⊆ On |
3 | | oveq2 7409 |
. . . . . . . 8
⊢ (𝑦 = 𝐷 → (𝐶 +o 𝑦) = (𝐶 +o 𝐷)) |
4 | 3 | sseq2d 4006 |
. . . . . . 7
⊢ (𝑦 = 𝐷 → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o 𝐷))) |
5 | | naddwordnex.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ On) |
6 | | naddwordnex.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝐷) |
7 | | onelon 6379 |
. . . . . . . . 9
⊢ ((𝐷 ∈ On ∧ 𝐶 ∈ 𝐷) → 𝐶 ∈ On) |
8 | 5, 6, 7 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ On) |
9 | | oaword2 8548 |
. . . . . . . 8
⊢ ((𝐷 ∈ On ∧ 𝐶 ∈ On) → 𝐷 ⊆ (𝐶 +o 𝐷)) |
10 | 5, 8, 9 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ (𝐶 +o 𝐷)) |
11 | 4, 5, 10 | elrabd 3677 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}) |
12 | 11, 1 | eleqtrrdi 2836 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑆) |
13 | 12 | ne0d 4327 |
. . . 4
⊢ (𝜑 → 𝑆 ≠ ∅) |
14 | | oninton 7776 |
. . . 4
⊢ ((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → ∩ 𝑆
∈ On) |
15 | 2, 13, 14 | sylancr 586 |
. . 3
⊢ (𝜑 → ∩ 𝑆
∈ On) |
16 | | oveq2 7409 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∅ → (𝐶 +o 𝑦) = (𝐶 +o ∅)) |
17 | | oa0 8511 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ On → (𝐶 +o ∅) = 𝐶) |
18 | 8, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 +o ∅) = 𝐶) |
19 | 16, 18 | sylan9eqr 2786 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐶 +o 𝑦) = 𝐶) |
20 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 = ∅) → 𝐶 ∈ 𝐷) |
21 | 19, 20 | eqeltrd 2825 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = ∅) → (𝐶 +o 𝑦) ∈ 𝐷) |
22 | 21 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 = ∅ → (𝐶 +o 𝑦) ∈ 𝐷)) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝑦 = ∅ → (𝐶 +o 𝑦) ∈ 𝐷)) |
24 | 23 | con3d 152 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (¬ (𝐶 +o 𝑦) ∈ 𝐷 → ¬ 𝑦 = ∅)) |
25 | | oacl 8530 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 +o 𝑦) ∈ On) |
26 | 8, 25 | sylan 579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐶 +o 𝑦) ∈ On) |
27 | | ontri1 6388 |
. . . . . . . . 9
⊢ ((𝐷 ∈ On ∧ (𝐶 +o 𝑦) ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ ¬ (𝐶 +o 𝑦) ∈ 𝐷)) |
28 | 5, 26, 27 | syl2an2r 682 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ ¬ (𝐶 +o 𝑦) ∈ 𝐷)) |
29 | | on0eln0 6410 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On → (∅
∈ 𝑦 ↔ 𝑦 ≠ ∅)) |
30 | | df-ne 2933 |
. . . . . . . . . 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 3137 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ On (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦)) |
36 | | 0ex 5297 |
. . . . . 6
⊢ ∅
∈ V |
37 | 36 | elintrab 4954 |
. . . . 5
⊢ (∅
∈ ∩ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} ↔ ∀𝑦 ∈ On (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦)) |
38 | 35, 37 | sylibr 233 |
. . . 4
⊢ (𝜑 → ∅ ∈ ∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)}) |
39 | 1 | inteqi 4944 |
. . . 4
⊢ ∩ 𝑆 =
∩ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} |
40 | 38, 39 | eleqtrrdi 2836 |
. . 3
⊢ (𝜑 → ∅ ∈ ∩ 𝑆) |
41 | | ondif1 8496 |
. . 3
⊢ (∩ 𝑆
∈ (On ∖ 1o) ↔ (∩ 𝑆 ∈ On ∧ ∅ ∈
∩ 𝑆)) |
42 | 15, 40, 41 | sylanbrc 582 |
. 2
⊢ (𝜑 → ∩ 𝑆
∈ (On ∖ 1o)) |
43 | | onzsl 7828 |
. . . . . 6
⊢ (∩ 𝑆
∈ On ↔ (∩ 𝑆 = ∅ ∨ ∃𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆))) |
44 | 15, 43 | sylib 217 |
. . . . 5
⊢ (𝜑 → (∩ 𝑆 =
∅ ∨ ∃𝑧
∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆))) |
45 | | oveq2 7409 |
. . . . . . . . 9
⊢ (∩ 𝑆 =
∅ → (𝐶
+o ∩ 𝑆) = (𝐶 +o ∅)) |
46 | 45, 18 | sylan9eqr 2786 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∩ 𝑆 =
∅) → (𝐶
+o ∩ 𝑆) = 𝐶) |
47 | | onelpss 6394 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → (𝐶 ∈ 𝐷 ↔ (𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷))) |
48 | 8, 5, 47 | syl2anc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 ∈ 𝐷 ↔ (𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷))) |
49 | 6, 48 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷)) |
50 | 49 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ⊆ 𝐷) |
51 | 50 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∩ 𝑆 =
∅) → 𝐶 ⊆
𝐷) |
52 | 46, 51 | eqsstrd 4012 |
. . . . . . 7
⊢ ((𝜑 ∧ ∩ 𝑆 =
∅) → (𝐶
+o ∩ 𝑆) ⊆ 𝐷) |
53 | 52 | ex 412 |
. . . . . 6
⊢ (𝜑 → (∩ 𝑆 =
∅ → (𝐶
+o ∩ 𝑆) ⊆ 𝐷)) |
54 | | oveq2 7409 |
. . . . . . . . 9
⊢ (∩ 𝑆 =
suc 𝑧 → (𝐶 +o ∩ 𝑆) =
(𝐶 +o suc 𝑧)) |
55 | | oasuc 8519 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ On ∧ 𝑧 ∈ On) → (𝐶 +o suc 𝑧) = suc (𝐶 +o 𝑧)) |
56 | 8, 55 | sylan 579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝐶 +o suc 𝑧) = suc (𝐶 +o 𝑧)) |
57 | 54, 56 | sylan9eqr 2786 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ ∩ 𝑆 =
suc 𝑧) → (𝐶 +o ∩ 𝑆) =
suc (𝐶 +o 𝑧)) |
58 | | vex 3470 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
59 | 58 | sucid 6436 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ suc 𝑧 |
60 | | eleq2 2814 |
. . . . . . . . . . . 12
⊢ (∩ 𝑆 =
suc 𝑧 → (𝑧 ∈ ∩ 𝑆
↔ 𝑧 ∈ suc 𝑧)) |
61 | 59, 60 | mpbiri 258 |
. . . . . . . . . . 11
⊢ (∩ 𝑆 =
suc 𝑧 → 𝑧 ∈ ∩ 𝑆) |
62 | 61 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∩ 𝑆 =
suc 𝑧 → 𝑧 ∈ ∩ 𝑆)) |
63 | 39 | eleq2i 2817 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∩ 𝑆
↔ 𝑧 ∈ ∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)}) |
64 | | oveq2 7409 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝐶 +o 𝑦) = (𝐶 +o 𝑧)) |
65 | 64 | sseq2d 4006 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o 𝑧))) |
66 | 65 | onnminsb 7780 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ On → (𝑧 ∈ ∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)} → ¬ 𝐷 ⊆ (𝐶 +o 𝑧))) |
67 | 66 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝑧 ∈ ∩ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → ¬ 𝐷 ⊆ (𝐶 +o 𝑧))) |
68 | 63, 67 | biimtrid 241 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝑧 ∈ ∩ 𝑆 → ¬ 𝐷 ⊆ (𝐶 +o 𝑧))) |
69 | | oacl 8530 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ On ∧ 𝑧 ∈ On) → (𝐶 +o 𝑧) ∈ On) |
70 | 8, 69 | sylan 579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝐶 +o 𝑧) ∈ On) |
71 | | ontri1 6388 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ On ∧ (𝐶 +o 𝑧) ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑧) ↔ ¬ (𝐶 +o 𝑧) ∈ 𝐷)) |
72 | 5, 70, 71 | syl2an2r 682 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑧) ↔ ¬ (𝐶 +o 𝑧) ∈ 𝐷)) |
73 | 72 | con2bid 354 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ On) → ((𝐶 +o 𝑧) ∈ 𝐷 ↔ ¬ 𝐷 ⊆ (𝐶 +o 𝑧))) |
74 | 68, 73 | sylibrd 259 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (𝑧 ∈ ∩ 𝑆 → (𝐶 +o 𝑧) ∈ 𝐷)) |
75 | | onsucss 42505 |
. . . . . . . . . . . 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 4012 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ On) ∧ ∩ 𝑆 =
suc 𝑧) → (𝐶 +o ∩ 𝑆)
⊆ 𝐷) |
81 | 80 | rexlimdva2 3149 |
. . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ On ∩ 𝑆 = suc 𝑧 → (𝐶 +o ∩
𝑆) ⊆ 𝐷)) |
82 | | oalim 8527 |
. . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → (𝐶 +o ∩
𝑆) = ∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧)) |
83 | 8, 82 | sylan 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → (𝐶 +o ∩
𝑆) = ∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧)) |
84 | | onelon 6379 |
. . . . . . . . . . . . . . 15
⊢ ((∩ 𝑆
∈ On ∧ 𝑧 ∈
∩ 𝑆) → 𝑧 ∈ On) |
85 | 15, 84 | sylan 579 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ ∩ 𝑆) → 𝑧 ∈ On) |
86 | 85 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑧 ∈ ∩ 𝑆 → 𝑧 ∈ On)) |
87 | 86 | ancrd 551 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ∈ ∩ 𝑆 → (𝑧 ∈ On ∧ 𝑧 ∈ ∩ 𝑆))) |
88 | 74 | expimpd 453 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑧 ∈ On ∧ 𝑧 ∈ ∩ 𝑆) → (𝐶 +o 𝑧) ∈ 𝐷)) |
89 | | onelss 6396 |
. . . . . . . . . . . . 13
⊢ (𝐷 ∈ On → ((𝐶 +o 𝑧) ∈ 𝐷 → (𝐶 +o 𝑧) ⊆ 𝐷)) |
90 | 5, 89 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 +o 𝑧) ∈ 𝐷 → (𝐶 +o 𝑧) ⊆ 𝐷)) |
91 | 87, 88, 90 | 3syld 60 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ∈ ∩ 𝑆 → (𝐶 +o 𝑧) ⊆ 𝐷)) |
92 | 91 | ralrimiv 3137 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷) |
93 | | iunss 5038 |
. . . . . . . . . 10
⊢ (∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷 ↔ ∀𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷) |
94 | 92, 93 | sylibr 233 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷) |
95 | 94 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → ∪ 𝑧 ∈ ∩ 𝑆(𝐶 +o 𝑧) ⊆ 𝐷) |
96 | 83, 95 | eqsstrd 4012 |
. . . . . . 7
⊢ ((𝜑 ∧ (∩ 𝑆
∈ V ∧ Lim ∩ 𝑆)) → (𝐶 +o ∩
𝑆) ⊆ 𝐷) |
97 | 96 | ex 412 |
. . . . . 6
⊢ (𝜑 → ((∩ 𝑆
∈ V ∧ Lim ∩ 𝑆) → (𝐶 +o ∩
𝑆) ⊆ 𝐷)) |
98 | 53, 81, 97 | 3jaod 1425 |
. . . . 5
⊢ (𝜑 → ((∩ 𝑆 =
∅ ∨ ∃𝑧
∈ On ∩ 𝑆 = suc 𝑧 ∨ (∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆))
→ (𝐶 +o
∩ 𝑆) ⊆ 𝐷)) |
99 | 44, 98 | mpd 15 |
. . . 4
⊢ (𝜑 → (𝐶 +o ∩
𝑆) ⊆ 𝐷) |
100 | 4 | rspcev 3604 |
. . . . . . 7
⊢ ((𝐷 ∈ On ∧ 𝐷 ⊆ (𝐶 +o 𝐷)) → ∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦)) |
101 | 5, 10, 100 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → ∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦)) |
102 | | nfcv 2895 |
. . . . . . . 8
⊢
Ⅎ𝑦𝐷 |
103 | | nfcv 2895 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐶 |
104 | | nfcv 2895 |
. . . . . . . . 9
⊢
Ⅎ𝑦
+o |
105 | | nfrab1 3443 |
. . . . . . . . . 10
⊢
Ⅎ𝑦{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} |
106 | 105 | nfint 4950 |
. . . . . . . . 9
⊢
Ⅎ𝑦∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)} |
107 | 103, 104,
106 | nfov 7431 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}) |
108 | 102, 107 | nfss 3966 |
. . . . . . 7
⊢
Ⅎ𝑦 𝐷 ⊆ (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}) |
109 | | oveq2 7409 |
. . . . . . . 8
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → (𝐶 +o 𝑦) = (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})) |
110 | 109 | sseq2d 4006 |
. . . . . . 7
⊢ (𝑦 = ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}))) |
111 | 108, 110 | onminsb 7775 |
. . . . . 6
⊢
(∃𝑦 ∈ On
𝐷 ⊆ (𝐶 +o 𝑦) → 𝐷 ⊆ (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})) |
112 | 101, 111 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆ (𝐶 +o ∩
{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})) |
113 | 39 | oveq2i 7412 |
. . . . 5
⊢ (𝐶 +o ∩ 𝑆) =
(𝐶 +o ∩ {𝑦
∈ On ∣ 𝐷 ⊆
(𝐶 +o 𝑦)}) |
114 | 112, 113 | sseqtrrdi 4025 |
. . . 4
⊢ (𝜑 → 𝐷 ⊆ (𝐶 +o ∩
𝑆)) |
115 | 99, 114 | eqssd 3991 |
. . 3
⊢ (𝜑 → (𝐶 +o ∩
𝑆) = 𝐷) |
116 | | omelon 9637 |
. . . . . 6
⊢ ω
∈ On |
117 | | omcl 8531 |
. . . . . 6
⊢ ((ω
∈ On ∧ 𝐷 ∈
On) → (ω ·o 𝐷) ∈ On) |
118 | 116, 5, 117 | sylancr 586 |
. . . . 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 6400 |
. . . . . . 7
⊢ (ω
∈ On → ((𝑁 ∈
𝑀 ∧ 𝑀 ∈ ω) → 𝑁 ∈ ω)) |
124 | 119, 122,
123 | sylc 65 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ω) |
125 | | nnon 7854 |
. . . . . 6
⊢ (𝑁 ∈ ω → 𝑁 ∈ On) |
126 | 124, 125 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ On) |
127 | | oaword1 8547 |
. . . . 5
⊢
(((ω ·o 𝐷) ∈ On ∧ 𝑁 ∈ On) → (ω
·o 𝐷)
⊆ ((ω ·o 𝐷) +o 𝑁)) |
128 | 118, 126,
127 | syl2anc 583 |
. . . 4
⊢ (𝜑 → (ω
·o 𝐷)
⊆ ((ω ·o 𝐷) +o 𝑁)) |
129 | | naddwordnex.a |
. . . . . 6
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) |
130 | 129 | oveq1d 7416 |
. . . . 5
⊢ (𝜑 → (𝐴 +o (ω ·o
∩ 𝑆)) = (((ω ·o 𝐶) +o 𝑀) +o (ω
·o ∩ 𝑆))) |
131 | | omcl 8531 |
. . . . . . 7
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ·o 𝐶) ∈ On) |
132 | 116, 8, 131 | sylancr 586 |
. . . . . 6
⊢ (𝜑 → (ω
·o 𝐶)
∈ On) |
133 | | nnon 7854 |
. . . . . . 7
⊢ (𝑀 ∈ ω → 𝑀 ∈ On) |
134 | 121, 133 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ On) |
135 | | omcl 8531 |
. . . . . . 7
⊢ ((ω
∈ On ∧ ∩ 𝑆 ∈ On) → (ω
·o ∩ 𝑆) ∈ On) |
136 | 116, 15, 135 | sylancr 586 |
. . . . . 6
⊢ (𝜑 → (ω
·o ∩ 𝑆) ∈ On) |
137 | | oaass 8556 |
. . . . . 6
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → (((ω
·o 𝐶)
+o 𝑀)
+o (ω ·o ∩ 𝑆)) = ((ω
·o 𝐶)
+o (𝑀
+o (ω ·o ∩ 𝑆)))) |
138 | 132, 134,
136, 137 | syl3anc 1368 |
. . . . 5
⊢ (𝜑 → (((ω
·o 𝐶)
+o 𝑀)
+o (ω ·o ∩ 𝑆)) = ((ω
·o 𝐶)
+o (𝑀
+o (ω ·o ∩ 𝑆)))) |
139 | 15, 116 | jctil 519 |
. . . . . . . . 9
⊢ (𝜑 → (ω ∈ On ∧
∩ 𝑆 ∈ On)) |
140 | | omword1 8568 |
. . . . . . . . 9
⊢
(((ω ∈ On ∧ ∩ 𝑆 ∈ On) ∧ ∅ ∈
∩ 𝑆) → ω ⊆ (ω
·o ∩ 𝑆)) |
141 | 139, 40, 140 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → ω ⊆ (ω
·o ∩ 𝑆)) |
142 | | oaabs 8643 |
. . . . . . . 8
⊢ (((𝑀 ∈ ω ∧ (ω
·o ∩ 𝑆) ∈ On) ∧ ω ⊆ (ω
·o ∩ 𝑆)) → (𝑀 +o (ω ·o
∩ 𝑆)) = (ω ·o ∩ 𝑆)) |
143 | 121, 136,
141, 142 | syl21anc 835 |
. . . . . . 7
⊢ (𝜑 → (𝑀 +o (ω ·o
∩ 𝑆)) = (ω ·o ∩ 𝑆)) |
144 | 143 | oveq2d 7417 |
. . . . . 6
⊢ (𝜑 → ((ω
·o 𝐶)
+o (𝑀
+o (ω ·o ∩ 𝑆))) = ((ω
·o 𝐶)
+o (ω ·o ∩ 𝑆))) |
145 | | odi 8574 |
. . . . . . 7
⊢ ((ω
∈ On ∧ 𝐶 ∈ On
∧ ∩ 𝑆 ∈ On) → (ω
·o (𝐶
+o ∩ 𝑆)) = ((ω ·o 𝐶) +o (ω
·o ∩ 𝑆))) |
146 | 119, 8, 15, 145 | syl3anc 1368 |
. . . . . 6
⊢ (𝜑 → (ω
·o (𝐶
+o ∩ 𝑆)) = ((ω ·o 𝐶) +o (ω
·o ∩ 𝑆))) |
147 | 115 | oveq2d 7417 |
. . . . . 6
⊢ (𝜑 → (ω
·o (𝐶
+o ∩ 𝑆)) = (ω ·o 𝐷)) |
148 | 144, 146,
147 | 3eqtr2d 2770 |
. . . . 5
⊢ (𝜑 → ((ω
·o 𝐶)
+o (𝑀
+o (ω ·o ∩ 𝑆))) = (ω
·o 𝐷)) |
149 | 130, 138,
148 | 3eqtrd 2768 |
. . . 4
⊢ (𝜑 → (𝐴 +o (ω ·o
∩ 𝑆)) = (ω ·o 𝐷)) |
150 | | naddwordnex.b |
. . . 4
⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) |
151 | 128, 149,
150 | 3sstr4d 4021 |
. . 3
⊢ (𝜑 → (𝐴 +o (ω ·o
∩ 𝑆)) ⊆ 𝐵) |
152 | | naddcl 8672 |
. . . . . . . 8
⊢
(((ω ·o 𝐶) ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) ∈ On) |
153 | 132, 136,
152 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) ∈ On) |
154 | 118, 153,
134 | 3jca 1125 |
. . . . . 6
⊢ (𝜑 → ((ω
·o 𝐷)
∈ On ∧ ((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
∈ On ∧ 𝑀 ∈
On)) |
155 | 147, 146 | eqtr3d 2766 |
. . . . . . 7
⊢ (𝜑 → (ω
·o 𝐷) =
((ω ·o 𝐶) +o (ω
·o ∩ 𝑆))) |
156 | | naddgeoa 42634 |
. . . . . . . 8
⊢
(((ω ·o 𝐶) ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → ((ω
·o 𝐶)
+o (ω ·o ∩ 𝑆)) ⊆ ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆))) |
157 | 132, 136,
156 | syl2anc 583 |
. . . . . . 7
⊢ (𝜑 → ((ω
·o 𝐶)
+o (ω ·o ∩ 𝑆)) ⊆ ((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆))) |
158 | 155, 157 | eqsstrd 4012 |
. . . . . 6
⊢ (𝜑 → (ω
·o 𝐷)
⊆ ((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))) |
159 | | oawordri 8545 |
. . . . . 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 42635 |
. . . . . . . . 9
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ ω) → ((ω
·o 𝐶)
+o 𝑀) =
((ω ·o 𝐶) +no 𝑀)) |
162 | 132, 121,
161 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → ((ω
·o 𝐶)
+o 𝑀) =
((ω ·o 𝐶) +no 𝑀)) |
163 | 129, 162 | eqtrd 2764 |
. . . . . . 7
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +no 𝑀)) |
164 | 163 | oveq1d 7416 |
. . . . . 6
⊢ (𝜑 → (𝐴 +no (ω ·o ∩ 𝑆))
= (((ω ·o 𝐶) +no 𝑀) +no (ω ·o ∩ 𝑆))) |
165 | | naddass 8691 |
. . . . . . . 8
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → (((ω
·o 𝐶) +no
𝑀) +no (ω
·o ∩ 𝑆)) = ((ω ·o 𝐶) +no (𝑀 +no (ω ·o ∩ 𝑆)))) |
166 | 132, 134,
136, 165 | syl3anc 1368 |
. . . . . . 7
⊢ (𝜑 → (((ω
·o 𝐶) +no
𝑀) +no (ω
·o ∩ 𝑆)) = ((ω ·o 𝐶) +no (𝑀 +no (ω ·o ∩ 𝑆)))) |
167 | | naddcom 8677 |
. . . . . . . . 9
⊢ ((𝑀 ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On) → (𝑀 +no (ω ·o ∩ 𝑆))
= ((ω ·o ∩ 𝑆) +no 𝑀)) |
168 | 134, 136,
167 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 +no (ω ·o ∩ 𝑆))
= ((ω ·o ∩ 𝑆) +no 𝑀)) |
169 | 168 | oveq2d 7417 |
. . . . . . 7
⊢ (𝜑 → ((ω
·o 𝐶) +no
(𝑀 +no (ω
·o ∩ 𝑆))) = ((ω ·o 𝐶) +no ((ω
·o ∩ 𝑆) +no 𝑀))) |
170 | | naddonnn 42635 |
. . . . . . . . 9
⊢
((((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
∈ On ∧ 𝑀 ∈
ω) → (((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
+o 𝑀) =
(((ω ·o 𝐶) +no (ω ·o ∩ 𝑆))
+no 𝑀)) |
171 | 153, 121,
170 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → (((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) +o 𝑀) = (((ω ·o 𝐶) +no (ω
·o ∩ 𝑆)) +no 𝑀)) |
172 | | naddass 8691 |
. . . . . . . . 9
⊢
(((ω ·o 𝐶) ∈ On ∧ (ω
·o ∩ 𝑆) ∈ On ∧ 𝑀 ∈ On) → (((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) +no 𝑀) = ((ω ·o 𝐶) +no ((ω
·o ∩ 𝑆) +no 𝑀))) |
173 | 132, 136,
134, 172 | syl3anc 1368 |
. . . . . . . 8
⊢ (𝜑 → (((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) +no 𝑀) = ((ω ·o 𝐶) +no ((ω
·o ∩ 𝑆) +no 𝑀))) |
174 | 171, 173 | eqtr2d 2765 |
. . . . . . 7
⊢ (𝜑 → ((ω
·o 𝐶) +no
((ω ·o ∩ 𝑆) +no 𝑀)) = (((ω ·o 𝐶) +no (ω
·o ∩ 𝑆)) +o 𝑀)) |
175 | 166, 169,
174 | 3eqtrd 2768 |
. . . . . 6
⊢ (𝜑 → (((ω
·o 𝐶) +no
𝑀) +no (ω
·o ∩ 𝑆)) = (((ω ·o 𝐶) +no (ω
·o ∩ 𝑆)) +o 𝑀)) |
176 | 164, 175 | eqtr2d 2765 |
. . . . 5
⊢ (𝜑 → (((ω
·o 𝐶) +no
(ω ·o ∩ 𝑆)) +o 𝑀) = (𝐴 +no (ω ·o ∩ 𝑆))) |
177 | 160, 176 | sseqtrd 4014 |
. . . 4
⊢ (𝜑 → ((ω
·o 𝐷)
+o 𝑀) ⊆
(𝐴 +no (ω
·o ∩ 𝑆))) |
178 | 134, 118 | jca 511 |
. . . . . 6
⊢ (𝜑 → (𝑀 ∈ On ∧ (ω
·o 𝐷)
∈ On)) |
179 | | oaordi 8541 |
. . . . . 6
⊢ ((𝑀 ∈ On ∧ (ω
·o 𝐷)
∈ On) → (𝑁 ∈
𝑀 → ((ω
·o 𝐷)
+o 𝑁) ∈
((ω ·o 𝐷) +o 𝑀))) |
180 | 178, 120,
179 | sylc 65 |
. . . . 5
⊢ (𝜑 → ((ω
·o 𝐷)
+o 𝑁) ∈
((ω ·o 𝐷) +o 𝑀)) |
181 | 150, 180 | eqeltrd 2825 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ((ω ·o 𝐷) +o 𝑀)) |
182 | 177, 181 | sseldd 3975 |
. . 3
⊢ (𝜑 → 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆))) |
183 | 115, 151,
182 | 3jca 1125 |
. 2
⊢ (𝜑 → ((𝐶 +o ∩
𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o
∩ 𝑆)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆)))) |
184 | | oveq2 7409 |
. . . . 5
⊢ (𝑥 = ∩
𝑆 → (𝐶 +o 𝑥) = (𝐶 +o ∩
𝑆)) |
185 | 184 | eqeq1d 2726 |
. . . 4
⊢ (𝑥 = ∩
𝑆 → ((𝐶 +o 𝑥) = 𝐷 ↔ (𝐶 +o ∩
𝑆) = 𝐷)) |
186 | | oveq2 7409 |
. . . . . 6
⊢ (𝑥 = ∩
𝑆 → (ω
·o 𝑥) =
(ω ·o ∩ 𝑆)) |
187 | 186 | oveq2d 7417 |
. . . . 5
⊢ (𝑥 = ∩
𝑆 → (𝐴 +o (ω ·o
𝑥)) = (𝐴 +o (ω ·o
∩ 𝑆))) |
188 | 187 | sseq1d 4005 |
. . . 4
⊢ (𝑥 = ∩
𝑆 → ((𝐴 +o (ω
·o 𝑥))
⊆ 𝐵 ↔ (𝐴 +o (ω
·o ∩ 𝑆)) ⊆ 𝐵)) |
189 | 186 | oveq2d 7417 |
. . . . 5
⊢ (𝑥 = ∩
𝑆 → (𝐴 +no (ω ·o 𝑥)) = (𝐴 +no (ω ·o ∩ 𝑆))) |
190 | 189 | eleq2d 2811 |
. . . 4
⊢ (𝑥 = ∩
𝑆 → (𝐵 ∈ (𝐴 +no (ω ·o 𝑥)) ↔ 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆)))) |
191 | 185, 188,
190 | 3anbi123d 1432 |
. . 3
⊢ (𝑥 = ∩
𝑆 → (((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o
𝑥)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o 𝑥))) ↔ ((𝐶 +o ∩
𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o
∩ 𝑆)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆))))) |
192 | 191 | rspcev 3604 |
. 2
⊢ ((∩ 𝑆
∈ (On ∖ 1o) ∧ ((𝐶 +o ∩
𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o
∩ 𝑆)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o ∩ 𝑆)))) → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o
𝑥)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o 𝑥)))) |
193 | 42, 183, 192 | syl2anc 583 |
1
⊢ (𝜑 → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o
𝑥)) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 +no (ω ·o 𝑥)))) |