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 42641
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 4072 . . . 4 𝑆 ⊆ On
3 oveq2 7409 . . . . . . . 8 (𝑦 = 𝐷 → (𝐶 +o 𝑦) = (𝐶 +o 𝐷))
43sseq2d 4006 . . . . . . 7 (𝑦 = 𝐷 → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o 𝐷)))
5 naddwordnex.d . . . . . . 7 (𝜑𝐷 ∈ On)
6 naddwordnex.c . . . . . . . . 9 (𝜑𝐶𝐷)
7 onelon 6379 . . . . . . . . 9 ((𝐷 ∈ On ∧ 𝐶𝐷) → 𝐶 ∈ On)
85, 6, 7syl2anc 583 . . . . . . . 8 (𝜑𝐶 ∈ On)
9 oaword2 8548 . . . . . . . 8 ((𝐷 ∈ On ∧ 𝐶 ∈ On) → 𝐷 ⊆ (𝐶 +o 𝐷))
105, 8, 9syl2anc 583 . . . . . . 7 (𝜑𝐷 ⊆ (𝐶 +o 𝐷))
114, 5, 10elrabd 3677 . . . . . 6 (𝜑𝐷 ∈ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
1211, 1eleqtrrdi 2836 . . . . 5 (𝜑𝐷𝑆)
1312ne0d 4327 . . . 4 (𝜑𝑆 ≠ ∅)
14 oninton 7776 . . . 4 ((𝑆 ⊆ On ∧ 𝑆 ≠ ∅) → 𝑆 ∈ On)
152, 13, 14sylancr 586 . . 3 (𝜑 𝑆 ∈ On)
16 oveq2 7409 . . . . . . . . . . . . 13 (𝑦 = ∅ → (𝐶 +o 𝑦) = (𝐶 +o ∅))
17 oa0 8511 . . . . . . . . . . . . . 14 (𝐶 ∈ On → (𝐶 +o ∅) = 𝐶)
188, 17syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐶 +o ∅) = 𝐶)
1916, 18sylan9eqr 2786 . . . . . . . . . . . 12 ((𝜑𝑦 = ∅) → (𝐶 +o 𝑦) = 𝐶)
206adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 = ∅) → 𝐶𝐷)
2119, 20eqeltrd 2825 . . . . . . . . . . 11 ((𝜑𝑦 = ∅) → (𝐶 +o 𝑦) ∈ 𝐷)
2221ex 412 . . . . . . . . . 10 (𝜑 → (𝑦 = ∅ → (𝐶 +o 𝑦) ∈ 𝐷))
2322adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ On) → (𝑦 = ∅ → (𝐶 +o 𝑦) ∈ 𝐷))
2423con3d 152 . . . . . . . 8 ((𝜑𝑦 ∈ On) → (¬ (𝐶 +o 𝑦) ∈ 𝐷 → ¬ 𝑦 = ∅))
25 oacl 8530 . . . . . . . . . 10 ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 +o 𝑦) ∈ On)
268, 25sylan 579 . . . . . . . . 9 ((𝜑𝑦 ∈ On) → (𝐶 +o 𝑦) ∈ On)
27 ontri1 6388 . . . . . . . . 9 ((𝐷 ∈ On ∧ (𝐶 +o 𝑦) ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ ¬ (𝐶 +o 𝑦) ∈ 𝐷))
285, 26, 27syl2an2r 682 . . . . . . . 8 ((𝜑𝑦 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ ¬ (𝐶 +o 𝑦) ∈ 𝐷))
29 on0eln0 6410 . . . . . . . . . 10 (𝑦 ∈ On → (∅ ∈ 𝑦𝑦 ≠ ∅))
30 df-ne 2933 . . . . . . . . . 10 (𝑦 ≠ ∅ ↔ ¬ 𝑦 = ∅)
3129, 30bitrdi 287 . . . . . . . . 9 (𝑦 ∈ On → (∅ ∈ 𝑦 ↔ ¬ 𝑦 = ∅))
3231adantl 481 . . . . . . . 8 ((𝜑𝑦 ∈ On) → (∅ ∈ 𝑦 ↔ ¬ 𝑦 = ∅))
3324, 28, 323imtr4d 294 . . . . . . 7 ((𝜑𝑦 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦))
3433ex 412 . . . . . 6 (𝜑 → (𝑦 ∈ On → (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦)))
3534ralrimiv 3137 . . . . 5 (𝜑 → ∀𝑦 ∈ On (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦))
36 0ex 5297 . . . . . 6 ∅ ∈ V
3736elintrab 4954 . . . . 5 (∅ ∈ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} ↔ ∀𝑦 ∈ On (𝐷 ⊆ (𝐶 +o 𝑦) → ∅ ∈ 𝑦))
3835, 37sylibr 233 . . . 4 (𝜑 → ∅ ∈ {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
391inteqi 4944 . . . 4 𝑆 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}
4038, 39eleqtrrdi 2836 . . 3 (𝜑 → ∅ ∈ 𝑆)
41 ondif1 8496 . . 3 ( 𝑆 ∈ (On ∖ 1o) ↔ ( 𝑆 ∈ On ∧ ∅ ∈ 𝑆))
4215, 40, 41sylanbrc 582 . 2 (𝜑 𝑆 ∈ (On ∖ 1o))
43 onzsl 7828 . . . . . 6 ( 𝑆 ∈ On ↔ ( 𝑆 = ∅ ∨ ∃𝑧 ∈ On 𝑆 = suc 𝑧 ∨ ( 𝑆 ∈ V ∧ Lim 𝑆)))
4415, 43sylib 217 . . . . 5 (𝜑 → ( 𝑆 = ∅ ∨ ∃𝑧 ∈ On 𝑆 = suc 𝑧 ∨ ( 𝑆 ∈ V ∧ Lim 𝑆)))
45 oveq2 7409 . . . . . . . . 9 ( 𝑆 = ∅ → (𝐶 +o 𝑆) = (𝐶 +o ∅))
4645, 18sylan9eqr 2786 . . . . . . . 8 ((𝜑 𝑆 = ∅) → (𝐶 +o 𝑆) = 𝐶)
47 onelpss 6394 . . . . . . . . . . . 12 ((𝐶 ∈ On ∧ 𝐷 ∈ On) → (𝐶𝐷 ↔ (𝐶𝐷𝐶𝐷)))
488, 5, 47syl2anc 583 . . . . . . . . . . 11 (𝜑 → (𝐶𝐷 ↔ (𝐶𝐷𝐶𝐷)))
496, 48mpbid 231 . . . . . . . . . 10 (𝜑 → (𝐶𝐷𝐶𝐷))
5049simpld 494 . . . . . . . . 9 (𝜑𝐶𝐷)
5150adantr 480 . . . . . . . 8 ((𝜑 𝑆 = ∅) → 𝐶𝐷)
5246, 51eqsstrd 4012 . . . . . . 7 ((𝜑 𝑆 = ∅) → (𝐶 +o 𝑆) ⊆ 𝐷)
5352ex 412 . . . . . 6 (𝜑 → ( 𝑆 = ∅ → (𝐶 +o 𝑆) ⊆ 𝐷))
54 oveq2 7409 . . . . . . . . 9 ( 𝑆 = suc 𝑧 → (𝐶 +o 𝑆) = (𝐶 +o suc 𝑧))
55 oasuc 8519 . . . . . . . . . 10 ((𝐶 ∈ On ∧ 𝑧 ∈ On) → (𝐶 +o suc 𝑧) = suc (𝐶 +o 𝑧))
568, 55sylan 579 . . . . . . . . 9 ((𝜑𝑧 ∈ On) → (𝐶 +o suc 𝑧) = suc (𝐶 +o 𝑧))
5754, 56sylan9eqr 2786 . . . . . . . 8 (((𝜑𝑧 ∈ On) ∧ 𝑆 = suc 𝑧) → (𝐶 +o 𝑆) = suc (𝐶 +o 𝑧))
58 vex 3470 . . . . . . . . . . . . 13 𝑧 ∈ V
5958sucid 6436 . . . . . . . . . . . 12 𝑧 ∈ suc 𝑧
60 eleq2 2814 . . . . . . . . . . . 12 ( 𝑆 = suc 𝑧 → (𝑧 𝑆𝑧 ∈ suc 𝑧))
6159, 60mpbiri 258 . . . . . . . . . . 11 ( 𝑆 = suc 𝑧𝑧 𝑆)
6261a1i 11 . . . . . . . . . 10 ((𝜑𝑧 ∈ On) → ( 𝑆 = suc 𝑧𝑧 𝑆))
6339eleq2i 2817 . . . . . . . . . . . 12 (𝑧 𝑆𝑧 {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
64 oveq2 7409 . . . . . . . . . . . . . . 15 (𝑦 = 𝑧 → (𝐶 +o 𝑦) = (𝐶 +o 𝑧))
6564sseq2d 4006 . . . . . . . . . . . . . 14 (𝑦 = 𝑧 → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o 𝑧)))
6665onnminsb 7780 . . . . . . . . . . . . 13 (𝑧 ∈ On → (𝑧 {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → ¬ 𝐷 ⊆ (𝐶 +o 𝑧)))
6766adantl 481 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ On) → (𝑧 {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → ¬ 𝐷 ⊆ (𝐶 +o 𝑧)))
6863, 67biimtrid 241 . . . . . . . . . . 11 ((𝜑𝑧 ∈ On) → (𝑧 𝑆 → ¬ 𝐷 ⊆ (𝐶 +o 𝑧)))
69 oacl 8530 . . . . . . . . . . . . . 14 ((𝐶 ∈ On ∧ 𝑧 ∈ On) → (𝐶 +o 𝑧) ∈ On)
708, 69sylan 579 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ On) → (𝐶 +o 𝑧) ∈ On)
71 ontri1 6388 . . . . . . . . . . . . 13 ((𝐷 ∈ On ∧ (𝐶 +o 𝑧) ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑧) ↔ ¬ (𝐶 +o 𝑧) ∈ 𝐷))
725, 70, 71syl2an2r 682 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ On) → (𝐷 ⊆ (𝐶 +o 𝑧) ↔ ¬ (𝐶 +o 𝑧) ∈ 𝐷))
7372con2bid 354 . . . . . . . . . . 11 ((𝜑𝑧 ∈ On) → ((𝐶 +o 𝑧) ∈ 𝐷 ↔ ¬ 𝐷 ⊆ (𝐶 +o 𝑧)))
7468, 73sylibrd 259 . . . . . . . . . 10 ((𝜑𝑧 ∈ On) → (𝑧 𝑆 → (𝐶 +o 𝑧) ∈ 𝐷))
75 onsucss 42505 . . . . . . . . . . . 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 4012 . . . . . . 7 (((𝜑𝑧 ∈ On) ∧ 𝑆 = suc 𝑧) → (𝐶 +o 𝑆) ⊆ 𝐷)
8180rexlimdva2 3149 . . . . . 6 (𝜑 → (∃𝑧 ∈ On 𝑆 = suc 𝑧 → (𝐶 +o 𝑆) ⊆ 𝐷))
82 oalim 8527 . . . . . . . . 9 ((𝐶 ∈ On ∧ ( 𝑆 ∈ V ∧ Lim 𝑆)) → (𝐶 +o 𝑆) = 𝑧 𝑆(𝐶 +o 𝑧))
838, 82sylan 579 . . . . . . . 8 ((𝜑 ∧ ( 𝑆 ∈ V ∧ Lim 𝑆)) → (𝐶 +o 𝑆) = 𝑧 𝑆(𝐶 +o 𝑧))
84 onelon 6379 . . . . . . . . . . . . . . 15 (( 𝑆 ∈ On ∧ 𝑧 𝑆) → 𝑧 ∈ On)
8515, 84sylan 579 . . . . . . . . . . . . . 14 ((𝜑𝑧 𝑆) → 𝑧 ∈ On)
8685ex 412 . . . . . . . . . . . . 13 (𝜑 → (𝑧 𝑆𝑧 ∈ On))
8786ancrd 551 . . . . . . . . . . . 12 (𝜑 → (𝑧 𝑆 → (𝑧 ∈ On ∧ 𝑧 𝑆)))
8874expimpd 453 . . . . . . . . . . . 12 (𝜑 → ((𝑧 ∈ On ∧ 𝑧 𝑆) → (𝐶 +o 𝑧) ∈ 𝐷))
89 onelss 6396 . . . . . . . . . . . . 13 (𝐷 ∈ On → ((𝐶 +o 𝑧) ∈ 𝐷 → (𝐶 +o 𝑧) ⊆ 𝐷))
905, 89syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐶 +o 𝑧) ∈ 𝐷 → (𝐶 +o 𝑧) ⊆ 𝐷))
9187, 88, 903syld 60 . . . . . . . . . . 11 (𝜑 → (𝑧 𝑆 → (𝐶 +o 𝑧) ⊆ 𝐷))
9291ralrimiv 3137 . . . . . . . . . 10 (𝜑 → ∀𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷)
93 iunss 5038 . . . . . . . . . 10 ( 𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷 ↔ ∀𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷)
9492, 93sylibr 233 . . . . . . . . 9 (𝜑 𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷)
9594adantr 480 . . . . . . . 8 ((𝜑 ∧ ( 𝑆 ∈ V ∧ Lim 𝑆)) → 𝑧 𝑆(𝐶 +o 𝑧) ⊆ 𝐷)
9683, 95eqsstrd 4012 . . . . . . 7 ((𝜑 ∧ ( 𝑆 ∈ V ∧ Lim 𝑆)) → (𝐶 +o 𝑆) ⊆ 𝐷)
9796ex 412 . . . . . 6 (𝜑 → (( 𝑆 ∈ V ∧ Lim 𝑆) → (𝐶 +o 𝑆) ⊆ 𝐷))
9853, 81, 973jaod 1425 . . . . 5 (𝜑 → (( 𝑆 = ∅ ∨ ∃𝑧 ∈ On 𝑆 = suc 𝑧 ∨ ( 𝑆 ∈ V ∧ Lim 𝑆)) → (𝐶 +o 𝑆) ⊆ 𝐷))
9944, 98mpd 15 . . . 4 (𝜑 → (𝐶 +o 𝑆) ⊆ 𝐷)
1004rspcev 3604 . . . . . . 7 ((𝐷 ∈ On ∧ 𝐷 ⊆ (𝐶 +o 𝐷)) → ∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦))
1015, 10, 100syl2anc 583 . . . . . 6 (𝜑 → ∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦))
102 nfcv 2895 . . . . . . . 8 𝑦𝐷
103 nfcv 2895 . . . . . . . . 9 𝑦𝐶
104 nfcv 2895 . . . . . . . . 9 𝑦 +o
105 nfrab1 3443 . . . . . . . . . 10 𝑦{𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}
106105nfint 4950 . . . . . . . . 9 𝑦 {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}
107103, 104, 106nfov 7431 . . . . . . . 8 𝑦(𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
108102, 107nfss 3966 . . . . . . 7 𝑦 𝐷 ⊆ (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
109 oveq2 7409 . . . . . . . 8 (𝑦 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → (𝐶 +o 𝑦) = (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}))
110109sseq2d 4006 . . . . . . 7 (𝑦 = {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)} → (𝐷 ⊆ (𝐶 +o 𝑦) ↔ 𝐷 ⊆ (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})))
111108, 110onminsb 7775 . . . . . 6 (∃𝑦 ∈ On 𝐷 ⊆ (𝐶 +o 𝑦) → 𝐷 ⊆ (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}))
112101, 111syl 17 . . . . 5 (𝜑𝐷 ⊆ (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)}))
11339oveq2i 7412 . . . . 5 (𝐶 +o 𝑆) = (𝐶 +o {𝑦 ∈ On ∣ 𝐷 ⊆ (𝐶 +o 𝑦)})
114112, 113sseqtrrdi 4025 . . . 4 (𝜑𝐷 ⊆ (𝐶 +o 𝑆))
11599, 114eqssd 3991 . . 3 (𝜑 → (𝐶 +o 𝑆) = 𝐷)
116 omelon 9637 . . . . . 6 ω ∈ On
117 omcl 8531 . . . . . 6 ((ω ∈ On ∧ 𝐷 ∈ On) → (ω ·o 𝐷) ∈ On)
118116, 5, 117sylancr 586 . . . . 5 (𝜑 → (ω ·o 𝐷) ∈ On)
119116a1i 11 . . . . . . 7 (𝜑 → ω ∈ On)
120 naddwordnex.n . . . . . . . 8 (𝜑𝑁𝑀)
121 naddwordnex.m . . . . . . . 8 (𝜑𝑀 ∈ ω)
122120, 121jca 511 . . . . . . 7 (𝜑 → (𝑁𝑀𝑀 ∈ ω))
123 ontr1 6400 . . . . . . 7 (ω ∈ On → ((𝑁𝑀𝑀 ∈ ω) → 𝑁 ∈ ω))
124119, 122, 123sylc 65 . . . . . 6 (𝜑𝑁 ∈ ω)
125 nnon 7854 . . . . . 6 (𝑁 ∈ ω → 𝑁 ∈ On)
126124, 125syl 17 . . . . 5 (𝜑𝑁 ∈ On)
127 oaword1 8547 . . . . 5 (((ω ·o 𝐷) ∈ On ∧ 𝑁 ∈ On) → (ω ·o 𝐷) ⊆ ((ω ·o 𝐷) +o 𝑁))
128118, 126, 127syl2anc 583 . . . 4 (𝜑 → (ω ·o 𝐷) ⊆ ((ω ·o 𝐷) +o 𝑁))
129 naddwordnex.a . . . . . 6 (𝜑𝐴 = ((ω ·o 𝐶) +o 𝑀))
130129oveq1d 7416 . . . . 5 (𝜑 → (𝐴 +o (ω ·o 𝑆)) = (((ω ·o 𝐶) +o 𝑀) +o (ω ·o 𝑆)))
131 omcl 8531 . . . . . . 7 ((ω ∈ On ∧ 𝐶 ∈ On) → (ω ·o 𝐶) ∈ On)
132116, 8, 131sylancr 586 . . . . . 6 (𝜑 → (ω ·o 𝐶) ∈ On)
133 nnon 7854 . . . . . . 7 (𝑀 ∈ ω → 𝑀 ∈ On)
134121, 133syl 17 . . . . . 6 (𝜑𝑀 ∈ On)
135 omcl 8531 . . . . . . 7 ((ω ∈ On ∧ 𝑆 ∈ On) → (ω ·o 𝑆) ∈ On)
136116, 15, 135sylancr 586 . . . . . 6 (𝜑 → (ω ·o 𝑆) ∈ On)
137 oaass 8556 . . . . . 6 (((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ (ω ·o 𝑆) ∈ On) → (((ω ·o 𝐶) +o 𝑀) +o (ω ·o 𝑆)) = ((ω ·o 𝐶) +o (𝑀 +o (ω ·o 𝑆))))
138132, 134, 136, 137syl3anc 1368 . . . . 5 (𝜑 → (((ω ·o 𝐶) +o 𝑀) +o (ω ·o 𝑆)) = ((ω ·o 𝐶) +o (𝑀 +o (ω ·o 𝑆))))
13915, 116jctil 519 . . . . . . . . 9 (𝜑 → (ω ∈ On ∧ 𝑆 ∈ On))
140 omword1 8568 . . . . . . . . 9 (((ω ∈ On ∧ 𝑆 ∈ On) ∧ ∅ ∈ 𝑆) → ω ⊆ (ω ·o 𝑆))
141139, 40, 140syl2anc 583 . . . . . . . 8 (𝜑 → ω ⊆ (ω ·o 𝑆))
142 oaabs 8643 . . . . . . . 8 (((𝑀 ∈ ω ∧ (ω ·o 𝑆) ∈ On) ∧ ω ⊆ (ω ·o 𝑆)) → (𝑀 +o (ω ·o 𝑆)) = (ω ·o 𝑆))
143121, 136, 141, 142syl21anc 835 . . . . . . 7 (𝜑 → (𝑀 +o (ω ·o 𝑆)) = (ω ·o 𝑆))
144143oveq2d 7417 . . . . . 6 (𝜑 → ((ω ·o 𝐶) +o (𝑀 +o (ω ·o 𝑆))) = ((ω ·o 𝐶) +o (ω ·o 𝑆)))
145 odi 8574 . . . . . . 7 ((ω ∈ On ∧ 𝐶 ∈ On ∧ 𝑆 ∈ On) → (ω ·o (𝐶 +o 𝑆)) = ((ω ·o 𝐶) +o (ω ·o 𝑆)))
146119, 8, 15, 145syl3anc 1368 . . . . . 6 (𝜑 → (ω ·o (𝐶 +o 𝑆)) = ((ω ·o 𝐶) +o (ω ·o 𝑆)))
147115oveq2d 7417 . . . . . 6 (𝜑 → (ω ·o (𝐶 +o 𝑆)) = (ω ·o 𝐷))
148144, 146, 1473eqtr2d 2770 . . . . 5 (𝜑 → ((ω ·o 𝐶) +o (𝑀 +o (ω ·o 𝑆))) = (ω ·o 𝐷))
149130, 138, 1483eqtrd 2768 . . . 4 (𝜑 → (𝐴 +o (ω ·o 𝑆)) = (ω ·o 𝐷))
150 naddwordnex.b . . . 4 (𝜑𝐵 = ((ω ·o 𝐷) +o 𝑁))
151128, 149, 1503sstr4d 4021 . . 3 (𝜑 → (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵)
152 naddcl 8672 . . . . . . . 8 (((ω ·o 𝐶) ∈ On ∧ (ω ·o 𝑆) ∈ On) → ((ω ·o 𝐶) +no (ω ·o 𝑆)) ∈ On)
153132, 136, 152syl2anc 583 . . . . . . 7 (𝜑 → ((ω ·o 𝐶) +no (ω ·o 𝑆)) ∈ On)
154118, 153, 1343jca 1125 . . . . . 6 (𝜑 → ((ω ·o 𝐷) ∈ On ∧ ((ω ·o 𝐶) +no (ω ·o 𝑆)) ∈ On ∧ 𝑀 ∈ On))
155147, 146eqtr3d 2766 . . . . . . 7 (𝜑 → (ω ·o 𝐷) = ((ω ·o 𝐶) +o (ω ·o 𝑆)))
156 naddgeoa 42634 . . . . . . . 8 (((ω ·o 𝐶) ∈ On ∧ (ω ·o 𝑆) ∈ On) → ((ω ·o 𝐶) +o (ω ·o 𝑆)) ⊆ ((ω ·o 𝐶) +no (ω ·o 𝑆)))
157132, 136, 156syl2anc 583 . . . . . . 7 (𝜑 → ((ω ·o 𝐶) +o (ω ·o 𝑆)) ⊆ ((ω ·o 𝐶) +no (ω ·o 𝑆)))
158155, 157eqsstrd 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 𝑀)))
160154, 158, 159sylc 65 . . . . 5 (𝜑 → ((ω ·o 𝐷) +o 𝑀) ⊆ (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀))
161 naddonnn 42635 . . . . . . . . 9 (((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ ω) → ((ω ·o 𝐶) +o 𝑀) = ((ω ·o 𝐶) +no 𝑀))
162132, 121, 161syl2anc 583 . . . . . . . 8 (𝜑 → ((ω ·o 𝐶) +o 𝑀) = ((ω ·o 𝐶) +no 𝑀))
163129, 162eqtrd 2764 . . . . . . 7 (𝜑𝐴 = ((ω ·o 𝐶) +no 𝑀))
164163oveq1d 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 𝑆))))
166132, 134, 136, 165syl3anc 1368 . . . . . . 7 (𝜑 → (((ω ·o 𝐶) +no 𝑀) +no (ω ·o 𝑆)) = ((ω ·o 𝐶) +no (𝑀 +no (ω ·o 𝑆))))
167 naddcom 8677 . . . . . . . . 9 ((𝑀 ∈ On ∧ (ω ·o 𝑆) ∈ On) → (𝑀 +no (ω ·o 𝑆)) = ((ω ·o 𝑆) +no 𝑀))
168134, 136, 167syl2anc 583 . . . . . . . 8 (𝜑 → (𝑀 +no (ω ·o 𝑆)) = ((ω ·o 𝑆) +no 𝑀))
169168oveq2d 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 𝑀))
171153, 121, 170syl2anc 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 𝑀)))
173132, 136, 134, 172syl3anc 1368 . . . . . . . 8 (𝜑 → (((ω ·o 𝐶) +no (ω ·o 𝑆)) +no 𝑀) = ((ω ·o 𝐶) +no ((ω ·o 𝑆) +no 𝑀)))
174171, 173eqtr2d 2765 . . . . . . 7 (𝜑 → ((ω ·o 𝐶) +no ((ω ·o 𝑆) +no 𝑀)) = (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀))
175166, 169, 1743eqtrd 2768 . . . . . 6 (𝜑 → (((ω ·o 𝐶) +no 𝑀) +no (ω ·o 𝑆)) = (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀))
176164, 175eqtr2d 2765 . . . . 5 (𝜑 → (((ω ·o 𝐶) +no (ω ·o 𝑆)) +o 𝑀) = (𝐴 +no (ω ·o 𝑆)))
177160, 176sseqtrd 4014 . . . 4 (𝜑 → ((ω ·o 𝐷) +o 𝑀) ⊆ (𝐴 +no (ω ·o 𝑆)))
178134, 118jca 511 . . . . . 6 (𝜑 → (𝑀 ∈ On ∧ (ω ·o 𝐷) ∈ On))
179 oaordi 8541 . . . . . 6 ((𝑀 ∈ On ∧ (ω ·o 𝐷) ∈ On) → (𝑁𝑀 → ((ω ·o 𝐷) +o 𝑁) ∈ ((ω ·o 𝐷) +o 𝑀)))
180178, 120, 179sylc 65 . . . . 5 (𝜑 → ((ω ·o 𝐷) +o 𝑁) ∈ ((ω ·o 𝐷) +o 𝑀))
181150, 180eqeltrd 2825 . . . 4 (𝜑𝐵 ∈ ((ω ·o 𝐷) +o 𝑀))
182177, 181sseldd 3975 . . 3 (𝜑𝐵 ∈ (𝐴 +no (ω ·o 𝑆)))
183115, 151, 1823jca 1125 . 2 (𝜑 → ((𝐶 +o 𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑆))))
184 oveq2 7409 . . . . 5 (𝑥 = 𝑆 → (𝐶 +o 𝑥) = (𝐶 +o 𝑆))
185184eqeq1d 2726 . . . 4 (𝑥 = 𝑆 → ((𝐶 +o 𝑥) = 𝐷 ↔ (𝐶 +o 𝑆) = 𝐷))
186 oveq2 7409 . . . . . 6 (𝑥 = 𝑆 → (ω ·o 𝑥) = (ω ·o 𝑆))
187186oveq2d 7417 . . . . 5 (𝑥 = 𝑆 → (𝐴 +o (ω ·o 𝑥)) = (𝐴 +o (ω ·o 𝑆)))
188187sseq1d 4005 . . . 4 (𝑥 = 𝑆 → ((𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵 ↔ (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵))
189186oveq2d 7417 . . . . 5 (𝑥 = 𝑆 → (𝐴 +no (ω ·o 𝑥)) = (𝐴 +no (ω ·o 𝑆)))
190189eleq2d 2811 . . . 4 (𝑥 = 𝑆 → (𝐵 ∈ (𝐴 +no (ω ·o 𝑥)) ↔ 𝐵 ∈ (𝐴 +no (ω ·o 𝑆))))
191185, 188, 1903anbi123d 1432 . . 3 (𝑥 = 𝑆 → (((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑥))) ↔ ((𝐶 +o 𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑆)))))
192191rspcev 3604 . 2 (( 𝑆 ∈ (On ∖ 1o) ∧ ((𝐶 +o 𝑆) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑆)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑆)))) → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑥))))
19342, 183, 192syl2anc 583 1 (𝜑 → ∃𝑥 ∈ (On ∖ 1o)((𝐶 +o 𝑥) = 𝐷 ∧ (𝐴 +o (ω ·o 𝑥)) ⊆ 𝐵𝐵 ∈ (𝐴 +no (ω ·o 𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3o 1083  w3a 1084   = wceq 1533  wcel 2098  wne 2932  wral 3053  wrex 3062  {crab 3424  Vcvv 3466  cdif 3937  wss 3940  c0 4314   cint 4940   ciun 4987  Oncon0 6354  Lim wlim 6355  suc csuc 6356  (class class class)co 7401  ωcom 7848  1oc1o 8454   +o coa 8458   ·o comu 8459   +no cnadd 8660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-ot 4629  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-omul 8466  df-nadd 8661
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator