Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  naddwordnexlem4 Structured version   Visualization version   GIF version

Theorem naddwordnexlem4 43391
Description: When 𝐴 is the sum of a limit ordinal (or zero) and a natural number and 𝐵 is the sum of a larger limit ordinal and a smaller natural number, there exists a product with omega such that the ordinal sum with 𝐴 is less than or equal to 𝐵 while the natural sum is larger than 𝐵. (Contributed by RP, 15-Feb-2025.)
Hypotheses
Ref Expression
naddwordnex.a (𝜑𝐴 = ((ω ·o 𝐶) +o 𝑀))
naddwordnex.b (𝜑𝐵 = ((ω ·o 𝐷) +o 𝑁))
naddwordnex.c (𝜑𝐶𝐷)
naddwordnex.d (𝜑𝐷 ∈ On)
naddwordnex.m (𝜑𝑀 ∈ ω)
naddwordnex.n (𝜑𝑁𝑀)
naddwordnexlem4.s 𝑆 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}
Assertion
Ref Expression
naddwordnexlem4 (𝜑 → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑥))))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝑆   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑦)   𝐵(𝑦)   𝑆(𝑦)   𝑀(𝑥,𝑦)   𝑁(𝑥,𝑦)

Proof of Theorem naddwordnexlem4
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 naddwordnexlem4.s . . . . 5 𝑆 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}
21ssrab3 4092 . . . 4 𝑆 ⊆ On
3 oveq2 7439 . . . . . . . 8 (𝑦 = 𝐷 → (𝐶 +o 𝑦) = (𝐶 +o 𝐷))
43sseq2d 4028 . . . . . . 7 (𝑦 = 𝐷 → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o 𝐷)))
5 naddwordnex.d . . . . . . 7 (𝜑𝐷 ∈ On)
6 naddwordnex.c . . . . . . . . 9 (𝜑𝐶𝐷)
7 onelon 6411 . . . . . . . . 9 ((𝐷 ∈ On ∧ 𝐶𝐷) → 𝐶 ∈ On)
85, 6, 7syl2anc 584 . . . . . . . 8 (𝜑𝐶 ∈ On)
9 oaword2 8590 . . . . . . . 8 ((𝐷 ∈ On ∧ 𝐶 ∈ On) → 𝐷 ⊆ (𝐶 +o 𝐷))
105, 8, 9syl2anc 584 . . . . . . 7 (𝜑𝐷 ⊆ (𝐶 +o 𝐷))
114, 5, 10elrabd 3697 . . . . . 6 (𝜑𝐷 ∈ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
1211, 1eleqtrrdi 2850 . . . . 5 (𝜑𝐷𝑆)
1312ne0d 4348 . . . 4 (𝜑𝑆 ≠ ∅)
14 oninton 7815 . . . 4 ((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → 𝑆 ∈ On)
152, 13, 14sylancr 587 . . 3 (𝜑 𝑆 ∈ On)
16 oveq2 7439 . . . . . . . . . . . . 13 (𝑦 = ∅ → (𝐶 +o 𝑦) = (𝐶 +o ∅))
17 oa0 8553 . . . . . . . . . . . . . 14 (𝐶 ∈ On → (𝐶 +o ∅) = 𝐶)
188, 17syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐶 +o ∅) = 𝐶)
1916, 18sylan9eqr 2797 . . . . . . . . . . . 12 ((𝜑𝑦 = ∅) → (𝐶 +o 𝑦) = 𝐶)
206adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 = ∅) → 𝐶𝐷)
2119, 20eqeltrd 2839 . . . . . . . . . . 11 ((𝜑𝑦 = ∅) → (𝐶 +o 𝑦) ∈ 𝐷)
2221ex 412 . . . . . . . . . 10 (𝜑 → (𝑦 = ∅ → (𝐶 +o 𝑦) ∈ 𝐷))
2322adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ On) → (𝑦 = ∅ → (𝐶 +o 𝑦) ∈ 𝐷))
2423con3d 152 . . . . . . . 8 ((𝜑𝑦 ∈ On) → (¬ (𝐶 +o 𝑦) ∈ 𝐷 → ¬ 𝑦 = ∅))
25 oacl 8572 . . . . . . . . . 10 ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 +o 𝑦) ∈ On)
268, 25sylan 580 . . . . . . . . 9 ((𝜑𝑦 ∈ On) → (𝐶 +o 𝑦) ∈ On)
27 ontri1 6420 . . . . . . . . 9 ((𝐷 ∈ On ∧ (𝐶 +o 𝑦) ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ ¬ (𝐶 +o 𝑦) ∈ 𝐷))
285, 26, 27syl2an2r 685 . . . . . . . 8 ((𝜑𝑦 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ ¬ (𝐶 +o 𝑦) ∈ 𝐷))
29 on0eln0 6442 . . . . . . . . . 10 (𝑦 ∈ On → (∅ ∈ 𝑦𝑦 ≠ ∅))
30 df-ne 2939 . . . . . . . . . 10 (𝑦 ≠ ∅ ↔ ¬ 𝑦 = ∅)
3129, 30bitrdi 287 . . . . . . . . 9 (𝑦 ∈ On → (∅ ∈ 𝑦 ↔ ¬ 𝑦 = ∅))
3231adantl 481 . . . . . . . 8 ((𝜑𝑦 ∈ On) → (∅ ∈ 𝑦 ↔ ¬ 𝑦 = ∅))
3324, 28, 323imtr4d 294 . . . . . . 7 ((𝜑𝑦 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦))
3433ex 412 . . . . . 6 (𝜑 → (𝑦 ∈ On → (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦)))
3534ralrimiv 3143 . . . . 5 (𝜑 → ∀𝑦 ∈ On (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦))
36 0ex 5313 . . . . . 6 ∅ ∈ V
3736elintrab 4965 . . . . 5 (∅ ∈ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} ↔ ∀𝑦 ∈ On (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦))
3835, 37sylibr 234 . . . 4 (𝜑 → ∅ ∈ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
391inteqi 4955 . . . 4 𝑆 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}
4038, 39eleqtrrdi 2850 . . 3 (𝜑 → ∅ ∈ 𝑆)
41 ondif1 8538 . . 3 ( 𝑆 ∈ (On ∖ 1o) ↔ ( 𝑆 ∈ On ∧ ∅ ∈ 𝑆))
4215, 40, 41sylanbrc 583 . 2 (𝜑 𝑆 ∈ (On ∖ 1o))
43 onzsl 7867 . . . . . 6 ( 𝑆 ∈ On ↔ ( 𝑆 = ∅ ∨ ∃𝑧 ∈ On 𝑆 = suc 𝑧 ∨ ( 𝑆 ∈ V ∧ Lim 𝑆)))
4415, 43sylib 218 . . . . 5 (𝜑 → ( 𝑆 = ∅ ∨ ∃𝑧 ∈ On 𝑆 = suc 𝑧 ∨ ( 𝑆 ∈ V ∧ Lim 𝑆)))
45 oveq2 7439 . . . . . . . . 9 ( 𝑆 = ∅ → (𝐶 +o 𝑆) = (𝐶 +o ∅))
4645, 18sylan9eqr 2797 . . . . . . . 8 ((𝜑 𝑆 = ∅) → (𝐶 +o 𝑆) = 𝐶)
47 onelpss 6426 . . . . . . . . . . . 12 ((𝐶 ∈ On ∧ 𝐷 ∈ On) → (𝐶𝐷 ↔ (𝐶𝐷𝐶𝐷)))
488, 5, 47syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐶𝐷 ↔ (𝐶𝐷𝐶𝐷)))
496, 48mpbid 232 . . . . . . . . . 10 (𝜑 → (𝐶𝐷𝐶𝐷))
5049simpld 494 . . . . . . . . 9 (𝜑𝐶𝐷)
5150adantr 480 . . . . . . . 8 ((𝜑 𝑆 = ∅) → 𝐶𝐷)
5246, 51eqsstrd 4034 . . . . . . 7 ((𝜑 𝑆 = ∅) → (𝐶 +o 𝑆) ⊆ 𝐷)
5352ex 412 . . . . . 6 (𝜑 → ( 𝑆 = ∅ → (𝐶 +o 𝑆) ⊆ 𝐷))
54 oveq2 7439 . . . . . . . . 9 ( 𝑆 = suc 𝑧 → (𝐶 +o 𝑆) = (𝐶 +o suc 𝑧))
55 oasuc 8561 . . . . . . . . . 10 ((𝐶 ∈ On ∧ 𝑧 ∈ On) → (𝐶 +o suc 𝑧) = suc (𝐶 +o 𝑧))
568, 55sylan 580 . . . . . . . . 9 ((𝜑𝑧 ∈ On) → (𝐶 +o suc 𝑧) = suc (𝐶 +o 𝑧))
5754, 56sylan9eqr 2797 . . . . . . . 8 (((𝜑𝑧 ∈ On) ∧ 𝑆 = suc 𝑧) → (𝐶 +o 𝑆) = suc (𝐶 +o 𝑧))
58 vex 3482 . . . . . . . . . . . . 13 𝑧 ∈ V
5958sucid 6468 . . . . . . . . . . . 12 𝑧 ∈ suc 𝑧
60 eleq2 2828 . . . . . . . . . . . 12 ( 𝑆 = suc 𝑧 → (𝑧 𝑆𝑧 ∈ suc 𝑧))
6159, 60mpbiri 258 . . . . . . . . . . 11 ( 𝑆 = suc 𝑧𝑧 𝑆)
6261a1i 11 . . . . . . . . . 10 ((𝜑𝑧 ∈ On) → ( 𝑆 = suc 𝑧𝑧 𝑆))
6339eleq2i 2831 . . . . . . . . . . . 12 (𝑧 𝑆𝑧 {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
64 oveq2 7439 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝐶 +o 𝑦) = (𝐶 +o 𝑧))
6564sseq2d 4028 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o 𝑧)))
6665onnminsb 7819 . . . . . . . . . . . . 13 (𝑧 ∈ On → (𝑧 {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → ¬ 𝐷 ⊆ (𝐶 +o 𝑧)))
6766adantl 481 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ On) → (𝑧 {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → ¬ 𝐷 ⊆ (𝐶 +o 𝑧)))
6863, 67biimtrid 242 . . . . . . . . . . 11 ((𝜑𝑧 ∈ On) → (𝑧 𝑆 → ¬ 𝐷 ⊆ (𝐶 +o 𝑧)))
69 oacl 8572 . . . . . . . . . . . . . 14 ((𝐶 ∈ On ∧ 𝑧 ∈ On) → (𝐶 +o 𝑧) ∈ On)
708, 69sylan 580 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ On) → (𝐶 +o 𝑧) ∈ On)
71 ontri1 6420 . . . . . . . . . . . . 13 ((𝐷 ∈ On ∧ (𝐶 +o 𝑧) ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑧) ↔ ¬ (𝐶 +o 𝑧) ∈ 𝐷))
725, 70, 71syl2an2r 685 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑧) ↔ ¬ (𝐶 +o 𝑧) ∈ 𝐷))
7372con2bid 354 . . . . . . . . . . 11 ((𝜑𝑧 ∈ On) → ((𝐶 +o 𝑧) ∈ 𝐷 ↔ ¬ 𝐷 ⊆ (𝐶 +o 𝑧)))
7468, 73sylibrd 259 . . . . . . . . . 10 ((𝜑𝑧 ∈ On) → (𝑧 𝑆 → (𝐶 +o 𝑧) ∈ 𝐷))
75 onsucss 43256 . . . . . . . . . . . 12 (𝐷 ∈ On → ((𝐶 +o 𝑧) ∈ 𝐷 → suc (𝐶 +o 𝑧) ⊆ 𝐷))
765, 75syl 17 . . . . . . . . . . 11 (𝜑 → ((𝐶 +o 𝑧) ∈ 𝐷 → suc (𝐶 +o 𝑧) ⊆ 𝐷))
7776adantr 480 . . . . . . . . . 10 ((𝜑𝑧 ∈ On) → ((𝐶 +o 𝑧) ∈ 𝐷 → suc (𝐶 +o 𝑧) ⊆ 𝐷))
7862, 74, 773syld 60 . . . . . . . . 9 ((𝜑𝑧 ∈ On) → ( 𝑆 = suc 𝑧 → suc (𝐶 +o 𝑧) ⊆ 𝐷))
7978imp 406 . . . . . . . 8 (((𝜑𝑧 ∈ On) ∧ 𝑆 = suc 𝑧) → suc (𝐶 +o 𝑧) ⊆ 𝐷)
8057, 79eqsstrd 4034 . . . . . . 7 (((𝜑𝑧 ∈ On) ∧ 𝑆 = suc 𝑧) → (𝐶 +o 𝑆) ⊆ 𝐷)
8180rexlimdva2 3155 . . . . . 6 (𝜑 → (∃𝑧 ∈ On 𝑆 = suc 𝑧 → (𝐶 +o 𝑆) ⊆ 𝐷))
82 oalim 8569 . . . . . . . . 9 ((𝐶 ∈ On ∧ ( 𝑆 ∈ V ∧ Lim 𝑆)) → (𝐶 +o 𝑆) = 𝑧 𝑆(𝐶 +o 𝑧))
838, 82sylan 580 . . . . . . . 8 ((𝜑 ∧ ( 𝑆 ∈ V ∧ Lim 𝑆)) → (𝐶 +o 𝑆) = 𝑧 𝑆(𝐶 +o 𝑧))
84 onelon 6411 . . . . . . . . . . . . . . 15 (( 𝑆 ∈ On ∧ 𝑧 𝑆) → 𝑧 ∈ On)
8515, 84sylan 580 . . . . . . . . . . . . . 14 ((𝜑𝑧 𝑆) → 𝑧 ∈ On)
8685ex 412 . . . . . . . . . . . . 13 (𝜑 → (𝑧 𝑆𝑧 ∈ On))
8786ancrd 551 . . . . . . . . . . . 12 (𝜑 → (𝑧 𝑆 → (𝑧 ∈ On ∧ 𝑧 𝑆)))
8874expimpd 453 . . . . . . . . . . . 12 (𝜑 → ((𝑧 ∈ On ∧ 𝑧 𝑆) → (𝐶 +o 𝑧) ∈ 𝐷))
89 onelss 6428 . . . . . . . . . . . . 13 (𝐷 ∈ On → ((𝐶 +o 𝑧) ∈ 𝐷 → (𝐶 +o 𝑧) ⊆ 𝐷))
905, 89syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐶 +o 𝑧) ∈ 𝐷 → (𝐶 +o 𝑧) ⊆ 𝐷))
9187, 88, 903syld 60 . . . . . . . . . . 11 (𝜑 → (𝑧 𝑆 → (𝐶 +o 𝑧) ⊆ 𝐷))
9291ralrimiv 3143 . . . . . . . . . 10 (𝜑 → ∀𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷)
93 iunss 5050 . . . . . . . . . 10 ( 𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷 ↔ ∀𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷)
9492, 93sylibr 234 . . . . . . . . 9 (𝜑 𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷)
9594adantr 480 . . . . . . . 8 ((𝜑 ∧ ( 𝑆 ∈ V ∧ Lim 𝑆)) → 𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷)
9683, 95eqsstrd 4034 . . . . . . 7 ((𝜑 ∧ ( 𝑆 ∈ V ∧ Lim 𝑆)) → (𝐶 +o 𝑆) ⊆ 𝐷)
9796ex 412 . . . . . 6 (𝜑 → (( 𝑆 ∈ V ∧ Lim 𝑆) → (𝐶 +o 𝑆) ⊆ 𝐷))
9853, 81, 973jaod 1428 . . . . 5 (𝜑 → (( 𝑆 = ∅ ∨ ∃𝑧 ∈ On 𝑆 = suc 𝑧 ∨ ( 𝑆 ∈ V ∧ Lim 𝑆)) → (𝐶 +o 𝑆) ⊆ 𝐷))
9944, 98mpd 15 . . . 4 (𝜑 → (𝐶 +o 𝑆) ⊆ 𝐷)
1004rspcev 3622 . . . . . . 7 ((𝐷 ∈ On ∧ 𝐷 ⊆ (𝐶 +o 𝐷)) → ∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦))
1015, 10, 100syl2anc 584 . . . . . 6 (𝜑 → ∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦))
102 nfcv 2903 . . . . . . . 8 𝑦𝐷
103 nfcv 2903 . . . . . . . . 9 𝑦𝐶
104 nfcv 2903 . . . . . . . . 9 𝑦 +o
105 nfrab1 3454 . . . . . . . . . 10 𝑦{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}
106105nfint 4961 . . . . . . . . 9 𝑦 {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}
107103, 104, 106nfov 7461 . . . . . . . 8 𝑦(𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
108102, 107nfss 3988 . . . . . . 7 𝑦 𝐷 ⊆ (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
109 oveq2 7439 . . . . . . . 8 (𝑦 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → (𝐶 +o 𝑦) = (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}))
110109sseq2d 4028 . . . . . . 7 (𝑦 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})))
111108, 110onminsb 7814 . . . . . 6 (∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦) → 𝐷 ⊆ (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}))
112101, 111syl 17 . . . . 5 (𝜑𝐷 ⊆ (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}))
11339oveq2i 7442 . . . . 5 (𝐶 +o 𝑆) = (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
114112, 113sseqtrrdi 4047 . . . 4 (𝜑𝐷 ⊆ (𝐶 +o 𝑆))
11599, 114eqssd 4013 . . 3 (𝜑 → (𝐶 +o 𝑆) = 𝐷)
116 omelon 9684 . . . . . 6 ω ∈ On
117 omcl 8573 . . . . . 6 ((ω ∈ On ∧ 𝐷 ∈ On) → (ω ·o 𝐷) ∈ On)
118116, 5, 117sylancr 587 . . . . 5 (𝜑 → (ω ·o 𝐷) ∈ On)
119116a1i 11 . . . . . . 7 (𝜑 → ω ∈ On)
120 naddwordnex.n . . . . . . . 8 (𝜑𝑁𝑀)
121 naddwordnex.m . . . . . . . 8 (𝜑𝑀 ∈ ω)
122120, 121jca 511 . . . . . . 7 (𝜑 → (𝑁𝑀𝑀 ∈ ω))
123 ontr1 6432 . . . . . . 7 (ω ∈ On → ((𝑁𝑀𝑀 ∈ ω) → 𝑁 ∈ ω))
124119, 122, 123sylc 65 . . . . . 6 (𝜑𝑁 ∈ ω)
125 nnon 7893 . . . . . 6 (𝑁 ∈ ω → 𝑁 ∈ On)
126124, 125syl 17 . . . . 5 (𝜑𝑁 ∈ On)
127 oaword1 8589 . . . . 5 (((ω ·o 𝐷) ∈ On ∧ 𝑁 ∈ On) → (ω ·o 𝐷) ⊆ ((ω ·o 𝐷) +o 𝑁))
128118, 126, 127syl2anc 584 . . . 4 (𝜑 → (ω ·o 𝐷) ⊆ ((ω ·o 𝐷) +o 𝑁))
129 naddwordnex.a . . . . . 6 (𝜑𝐴 = ((ω ·o 𝐶) +o 𝑀))
130129oveq1d 7446 . . . . 5 (𝜑 → (𝐴 +o (ω ·o 𝑆)) = (((ω ·o 𝐶) +o 𝑀) +o (ω ·o 𝑆)))
131 omcl 8573 . . . . . . 7 ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ·o 𝐶) ∈ On)
132116, 8, 131sylancr 587 . . . . . 6 (𝜑 → (ω ·o 𝐶) ∈ On)
133 nnon 7893 . . . . . . 7 (𝑀 ∈ ω → 𝑀 ∈ On)
134121, 133syl 17 . . . . . 6 (𝜑𝑀 ∈ On)
135 omcl 8573 . . . . . . 7 ((ω ∈ On ∧ 𝑆 ∈ On) → (ω ·o 𝑆) ∈ On)
136116, 15, 135sylancr 587 . . . . . 6 (𝜑 → (ω ·o 𝑆) ∈ On)
137 oaass 8598 . . . . . 6 (((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ (ω ·o 𝑆) ∈ On) → (((ω ·o 𝐶) +o 𝑀) +o (ω ·o 𝑆)) = ((ω ·o 𝐶) +o (𝑀 +o (ω ·o 𝑆))))
138132, 134, 136, 137syl3anc 1370 . . . . 5 (𝜑 → (((ω ·o 𝐶) +o 𝑀) +o (ω ·o 𝑆)) = ((ω ·o 𝐶) +o (𝑀 +o (ω ·o 𝑆))))
13915, 116jctil 519 . . . . . . . . 9 (𝜑 → (ω ∈ On ∧ 𝑆 ∈ On))
140 omword1 8610 . . . . . . . . 9 (((ω ∈ On ∧ 𝑆 ∈ On) ∧ ∅ ∈ 𝑆) → ω ⊆ (ω ·o 𝑆))
141139, 40, 140syl2anc 584 . . . . . . . 8 (𝜑 → ω ⊆ (ω ·o 𝑆))
142 oaabs 8685 . . . . . . . 8 (((𝑀 ∈ ω ∧ (ω ·o 𝑆) ∈ On) ∧ ω ⊆ (ω ·o 𝑆)) → (𝑀 +o (ω ·o 𝑆)) = (ω ·o 𝑆))
143121, 136, 141, 142syl21anc 838 . . . . . . 7 (𝜑 → (𝑀 +o (ω ·o 𝑆)) = (ω ·o 𝑆))
144143oveq2d 7447 . . . . . 6 (𝜑 → ((ω ·o 𝐶) +o (𝑀 +o (ω ·o 𝑆))) = ((ω ·o 𝐶) +o (ω ·o 𝑆)))
145 odi 8616 . . . . . . 7 ((ω ∈ On ∧ 𝐶 ∈ On ∧ 𝑆 ∈ On) → (ω ·o (𝐶 +o 𝑆)) = ((ω ·o 𝐶) +o (ω ·o 𝑆)))
146119, 8, 15, 145syl3anc 1370 . . . . . 6 (𝜑 → (ω ·o (𝐶 +o 𝑆)) = ((ω ·o 𝐶) +o (ω ·o 𝑆)))
147115oveq2d 7447 . . . . . 6 (𝜑 → (ω ·o (𝐶 +o 𝑆)) = (ω ·o 𝐷))
148144, 146, 1473eqtr2d 2781 . . . . 5 (𝜑 → ((ω ·o 𝐶) +o (𝑀 +o (ω ·o 𝑆))) = (ω ·o 𝐷))
149130, 138, 1483eqtrd 2779 . . . 4 (𝜑 → (𝐴 +o (ω ·o 𝑆)) = (ω ·o 𝐷))
150 naddwordnex.b . . . 4 (𝜑𝐵 = ((ω ·o 𝐷) +o 𝑁))
151128, 149, 1503sstr4d 4043 . . 3 (𝜑 → (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵)
152 naddcl 8714 . . . . . . . 8 (((ω ·o 𝐶) ∈ On ∧ (ω ·o 𝑆) ∈ On) → ((ω ·o 𝐶) +no (ω ·o 𝑆)) ∈ On)
153132, 136, 152syl2anc 584 . . . . . . 7 (𝜑 → ((ω ·o 𝐶) +no (ω ·o 𝑆)) ∈ On)
154118, 153, 1343jca 1127 . . . . . 6 (𝜑 → ((ω ·o 𝐷) ∈ On ∧ ((ω ·o 𝐶) +no (ω ·o 𝑆)) ∈ On ∧ 𝑀 ∈ On))
155147, 146eqtr3d 2777 . . . . . . 7 (𝜑 → (ω ·o 𝐷) = ((ω ·o 𝐶) +o (ω ·o 𝑆)))
156 naddgeoa 43384 . . . . . . . 8 (((ω ·o 𝐶) ∈ On ∧ (ω ·o 𝑆) ∈ On) → ((ω ·o 𝐶) +o (ω ·o 𝑆)) ⊆ ((ω ·o 𝐶) +no (ω ·o 𝑆)))
157132, 136, 156syl2anc 584 . . . . . . 7 (𝜑 → ((ω ·o 𝐶) +o (ω ·o 𝑆)) ⊆ ((ω ·o 𝐶) +no (ω ·o 𝑆)))
158155, 157eqsstrd 4034 . . . . . 6 (𝜑 → (ω ·o 𝐷) ⊆ ((ω ·o 𝐶) +no (ω ·o 𝑆)))
159 oawordri 8587 . . . . . 6 (((ω ·o 𝐷) ∈ On ∧ ((ω ·o 𝐶) +no (ω ·o 𝑆)) ∈ On ∧ 𝑀 ∈ On) → ((ω ·o 𝐷) ⊆ ((ω ·o 𝐶) +no (ω ·o 𝑆)) → ((ω ·o 𝐷) +o 𝑀) ⊆ (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀)))
160154, 158, 159sylc 65 . . . . 5 (𝜑 → ((ω ·o 𝐷) +o 𝑀) ⊆ (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀))
161 naddonnn 43385 . . . . . . . . 9 (((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ ω) → ((ω ·o 𝐶) +o 𝑀) = ((ω ·o 𝐶) +no 𝑀))
162132, 121, 161syl2anc 584 . . . . . . . 8 (𝜑 → ((ω ·o 𝐶) +o 𝑀) = ((ω ·o 𝐶) +no 𝑀))
163129, 162eqtrd 2775 . . . . . . 7 (𝜑𝐴 = ((ω ·o 𝐶) +no 𝑀))
164163oveq1d 7446 . . . . . 6 (𝜑 → (𝐴 +no (ω ·o 𝑆)) = (((ω ·o 𝐶) +no 𝑀) +no (ω ·o 𝑆)))
165 naddass 8733 . . . . . . . 8 (((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ (ω ·o 𝑆) ∈ On) → (((ω ·o 𝐶) +no 𝑀) +no (ω ·o 𝑆)) = ((ω ·o 𝐶) +no (𝑀 +no (ω ·o 𝑆))))
166132, 134, 136, 165syl3anc 1370 . . . . . . 7 (𝜑 → (((ω ·o 𝐶) +no 𝑀) +no (ω ·o 𝑆)) = ((ω ·o 𝐶) +no (𝑀 +no (ω ·o 𝑆))))
167 naddcom 8719 . . . . . . . . 9 ((𝑀 ∈ On ∧ (ω ·o 𝑆) ∈ On) → (𝑀 +no (ω ·o 𝑆)) = ((ω ·o 𝑆) +no 𝑀))
168134, 136, 167syl2anc 584 . . . . . . . 8 (𝜑 → (𝑀 +no (ω ·o 𝑆)) = ((ω ·o 𝑆) +no 𝑀))
169168oveq2d 7447 . . . . . . 7 (𝜑 → ((ω ·o 𝐶) +no (𝑀 +no (ω ·o 𝑆))) = ((ω ·o 𝐶) +no ((ω ·o 𝑆) +no 𝑀)))
170 naddonnn 43385 . . . . . . . . 9 ((((ω ·o 𝐶) +no (ω ·o 𝑆)) ∈ On ∧ 𝑀 ∈ ω) → (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀) = (((ω ·o 𝐶) +no (ω ·o 𝑆)) +no 𝑀))
171153, 121, 170syl2anc 584 . . . . . . . 8 (𝜑 → (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀) = (((ω ·o 𝐶) +no (ω ·o 𝑆)) +no 𝑀))
172 naddass 8733 . . . . . . . . 9 (((ω ·o 𝐶) ∈ On ∧ (ω ·o 𝑆) ∈ On ∧ 𝑀 ∈ On) → (((ω ·o 𝐶) +no (ω ·o 𝑆)) +no 𝑀) = ((ω ·o 𝐶) +no ((ω ·o 𝑆) +no 𝑀)))
173132, 136, 134, 172syl3anc 1370 . . . . . . . 8 (𝜑 → (((ω ·o 𝐶) +no (ω ·o 𝑆)) +no 𝑀) = ((ω ·o 𝐶) +no ((ω ·o 𝑆) +no 𝑀)))
174171, 173eqtr2d 2776 . . . . . . 7 (𝜑 → ((ω ·o 𝐶) +no ((ω ·o 𝑆) +no 𝑀)) = (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀))
175166, 169, 1743eqtrd 2779 . . . . . 6 (𝜑 → (((ω ·o 𝐶) +no 𝑀) +no (ω ·o 𝑆)) = (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀))
176164, 175eqtr2d 2776 . . . . 5 (𝜑 → (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀) = (𝐴 +no (ω ·o 𝑆)))
177160, 176sseqtrd 4036 . . . 4 (𝜑 → ((ω ·o 𝐷) +o 𝑀) ⊆ (𝐴 +no (ω ·o 𝑆)))
178134, 118jca 511 . . . . . 6 (𝜑 → (𝑀 ∈ On ∧ (ω ·o 𝐷) ∈ On))
179 oaordi 8583 . . . . . 6 ((𝑀 ∈ On ∧ (ω ·o 𝐷) ∈ On) → (𝑁𝑀 → ((ω ·o 𝐷) +o 𝑁) ∈ ((ω ·o 𝐷) +o 𝑀)))
180178, 120, 179sylc 65 . . . . 5 (𝜑 → ((ω ·o 𝐷) +o 𝑁) ∈ ((ω ·o 𝐷) +o 𝑀))
181150, 180eqeltrd 2839 . . . 4 (𝜑𝐵 ∈ ((ω ·o 𝐷) +o 𝑀))
182177, 181sseldd 3996 . . 3 (𝜑𝐵 ∈ (𝐴 +no (ω ·o 𝑆)))
183115, 151, 1823jca 1127 . 2 (𝜑 → ((𝐶 +o 𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑆))))
184 oveq2 7439 . . . . 5 (𝑥 = 𝑆 → (𝐶 +o 𝑥) = (𝐶 +o 𝑆))
185184eqeq1d 2737 . . . 4 (𝑥 = 𝑆 → ((𝐶 +o 𝑥) = 𝐷 ↔ (𝐶 +o 𝑆) = 𝐷))
186 oveq2 7439 . . . . . 6 (𝑥 = 𝑆 → (ω ·o 𝑥) = (ω ·o 𝑆))
187186oveq2d 7447 . . . . 5 (𝑥 = 𝑆 → (𝐴 +o (ω ·o 𝑥)) = (𝐴 +o (ω ·o 𝑆)))
188187sseq1d 4027 . . . 4 (𝑥 = 𝑆 → ((𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵 ↔ (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵))
189186oveq2d 7447 . . . . 5 (𝑥 = 𝑆 → (𝐴 +no (ω ·o 𝑥)) = (𝐴 +no (ω ·o 𝑆)))
190189eleq2d 2825 . . . 4 (𝑥 = 𝑆 → (𝐵 ∈ (𝐴 +no (ω ·o 𝑥)) ↔ 𝐵 ∈ (𝐴 +no (ω ·o 𝑆))))
191185, 188, 1903anbi123d 1435 . . 3 (𝑥 = 𝑆 → (((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑥))) ↔ ((𝐶 +o 𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑆)))))
192191rspcev 3622 . 2 (( 𝑆 ∈ (On ∖ 1o) ∧ ((𝐶 +o 𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑆)))) → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑥))))
19342, 183, 192syl2anc 584 1 (𝜑 → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3o 1085  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wral 3059  wrex 3068  {crab 3433  Vcvv 3478  cdif 3960  wss 3963  c0 4339   cint 4951   ciun 4996  Oncon0 6386  Lim wlim 6387  suc csuc 6388  (class class class)co 7431  ωcom 7887  1oc1o 8498   +o coa 8502   ·o comu 8503   +no cnadd 8702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-ot 4640  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-oadd 8509  df-omul 8510  df-nadd 8703
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator