Metamath Proof Explorer

Theorem naddwordnexlem4

Description: When A is the sum of a limit ordinal (or zero) and a natural number and B 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 A is less than or equal to B while the natural sum is larger than B . (Contributed by RP, 15-Feb-2025)

Ref Expression
Hypotheses naddwordnex.a ⊢ ( 𝜑 → 𝐴 = ( ( ω ·o 𝐶 ) +o 𝑀 ) )
naddwordnex.b ⊢ ( 𝜑 → 𝐵 = ( ( ω ·o 𝐷 ) +o 𝑁 ) )
naddwordnex.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
naddwordnex.d ⊢ ( 𝜑 → 𝐷 ∈ On )
naddwordnex.m ⊢ ( 𝜑 → 𝑀 ∈ ω )
naddwordnex.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑀 )
naddwordnexlem4.s ⊢ 𝑆 = { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) }
Assertion naddwordnexlem4 ( 𝜑 → ∃ 𝑥 ∈ ( On ∖ 1o ) ( ( 𝐶 +o 𝑥 ) = 𝐷 ∧ ( 𝐴 +o ( ω ·o 𝑥 ) ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +no ( ω ·o 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 naddwordnex.a ⊢ ( 𝜑 → 𝐴 = ( ( ω ·o 𝐶 ) +o 𝑀 ) )
2 naddwordnex.b ⊢ ( 𝜑 → 𝐵 = ( ( ω ·o 𝐷 ) +o 𝑁 ) )
3 naddwordnex.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
4 naddwordnex.d ⊢ ( 𝜑 → 𝐷 ∈ On )
5 naddwordnex.m ⊢ ( 𝜑 → 𝑀 ∈ ω )
6 naddwordnex.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑀 )
7 naddwordnexlem4.s ⊢ 𝑆 = { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) }
8 7 ssrab3 ⊢ 𝑆 ⊆ On
9 oveq2 ⊢ ( 𝑦 = 𝐷 → ( 𝐶 +o 𝑦 ) = ( 𝐶 +o 𝐷 ) )
10 9 sseq2d ⊢ ( 𝑦 = 𝐷 → ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) ↔ 𝐷 ⊆ ( 𝐶 +o 𝐷 ) ) )
11 onelon ⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ On )
12 4 3 11 syl2anc ⊢ ( 𝜑 → 𝐶 ∈ On )
13 oaword2 ⊢ ( ( 𝐷 ∈ On ∧ 𝐶 ∈ On ) → 𝐷 ⊆ ( 𝐶 +o 𝐷 ) )
14 4 12 13 syl2anc ⊢ ( 𝜑 → 𝐷 ⊆ ( 𝐶 +o 𝐷 ) )
15 10 4 14 elrabd ⊢ ( 𝜑 → 𝐷 ∈ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } )
16 15 7 eleqtrrdi ⊢ ( 𝜑 → 𝐷 ∈ 𝑆 )
17 16 ne0d ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
18 oninton ⊢ ( ( 𝑆 ⊆ On ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ On )
19 8 17 18 sylancr ⊢ ( 𝜑 → ∩ 𝑆 ∈ On )
20 oveq2 ⊢ ( 𝑦 = ∅ → ( 𝐶 +o 𝑦 ) = ( 𝐶 +o ∅ ) )
21 oa0 ⊢ ( 𝐶 ∈ On → ( 𝐶 +o ∅ ) = 𝐶 )
22 12 21 syl ⊢ ( 𝜑 → ( 𝐶 +o ∅ ) = 𝐶 )
23 20 22 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝐶 +o 𝑦 ) = 𝐶 )
24 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → 𝐶 ∈ 𝐷 )
25 23 24 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ( 𝐶 +o 𝑦 ) ∈ 𝐷 )
26 25 ex ⊢ ( 𝜑 → ( 𝑦 = ∅ → ( 𝐶 +o 𝑦 ) ∈ 𝐷 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( 𝑦 = ∅ → ( 𝐶 +o 𝑦 ) ∈ 𝐷 ) )
28 27 con3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( ¬ ( 𝐶 +o 𝑦 ) ∈ 𝐷 → ¬ 𝑦 = ∅ ) )
29 oacl ⊢ ( ( 𝐶 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐶 +o 𝑦 ) ∈ On )
30 12 29 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( 𝐶 +o 𝑦 ) ∈ On )
31 ontri1 ⊢ ( ( 𝐷 ∈ On ∧ ( 𝐶 +o 𝑦 ) ∈ On ) → ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) ↔ ¬ ( 𝐶 +o 𝑦 ) ∈ 𝐷 ) )
32 4 30 31 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) ↔ ¬ ( 𝐶 +o 𝑦 ) ∈ 𝐷 ) )
33 on0eln0 ⊢ ( 𝑦 ∈ On → ( ∅ ∈ 𝑦 ↔ 𝑦 ≠ ∅ ) )
34 df-ne ⊢ ( 𝑦 ≠ ∅ ↔ ¬ 𝑦 = ∅ )
35 33 34 bitrdi ⊢ ( 𝑦 ∈ On → ( ∅ ∈ 𝑦 ↔ ¬ 𝑦 = ∅ ) )
36 35 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( ∅ ∈ 𝑦 ↔ ¬ 𝑦 = ∅ ) )
37 28 32 36 3imtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ On ) → ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) → ∅ ∈ 𝑦 ) )
38 37 ex ⊢ ( 𝜑 → ( 𝑦 ∈ On → ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) → ∅ ∈ 𝑦 ) ) )
39 38 ralrimiv ⊢ ( 𝜑 → ∀ 𝑦 ∈ On ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) → ∅ ∈ 𝑦 ) )
40 0ex ⊢ ∅ ∈ V
41 40 elintrab ⊢ ( ∅ ∈ ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } ↔ ∀ 𝑦 ∈ On ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) → ∅ ∈ 𝑦 ) )
42 39 41 sylibr ⊢ ( 𝜑 → ∅ ∈ ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } )
43 7 inteqi ⊢ ∩ 𝑆 = ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) }
44 42 43 eleqtrrdi ⊢ ( 𝜑 → ∅ ∈ ∩ 𝑆 )
45 ondif1 ⊢ ( ∩ 𝑆 ∈ ( On ∖ 1o ) ↔ ( ∩ 𝑆 ∈ On ∧ ∅ ∈ ∩ 𝑆 ) )
46 19 44 45 sylanbrc ⊢ ( 𝜑 → ∩ 𝑆 ∈ ( On ∖ 1o ) )
47 onzsl ⊢ ( ∩ 𝑆 ∈ On ↔ ( ∩ 𝑆 = ∅ ∨ ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) )
48 19 47 sylib ⊢ ( 𝜑 → ( ∩ 𝑆 = ∅ ∨ ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) )
49 oveq2 ⊢ ( ∩ 𝑆 = ∅ → ( 𝐶 +o ∩ 𝑆 ) = ( 𝐶 +o ∅ ) )
50 49 22 sylan9eqr ⊢ ( ( 𝜑 ∧ ∩ 𝑆 = ∅ ) → ( 𝐶 +o ∩ 𝑆 ) = 𝐶 )
51 onelpss ⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 ∈ 𝐷 ↔ ( 𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) )
52 12 4 51 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ 𝐷 ↔ ( 𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷 ) ) )
53 3 52 mpbid ⊢ ( 𝜑 → ( 𝐶 ⊆ 𝐷 ∧ 𝐶 ≠ 𝐷 ) )
54 53 simpld ⊢ ( 𝜑 → 𝐶 ⊆ 𝐷 )
55 54 adantr ⊢ ( ( 𝜑 ∧ ∩ 𝑆 = ∅ ) → 𝐶 ⊆ 𝐷 )
56 50 55 eqsstrd ⊢ ( ( 𝜑 ∧ ∩ 𝑆 = ∅ ) → ( 𝐶 +o ∩ 𝑆 ) ⊆ 𝐷 )
57 56 ex ⊢ ( 𝜑 → ( ∩ 𝑆 = ∅ → ( 𝐶 +o ∩ 𝑆 ) ⊆ 𝐷 ) )
58 oveq2 ⊢ ( ∩ 𝑆 = suc 𝑧 → ( 𝐶 +o ∩ 𝑆 ) = ( 𝐶 +o suc 𝑧 ) )
59 oasuc ⊢ ( ( 𝐶 ∈ On ∧ 𝑧 ∈ On ) → ( 𝐶 +o suc 𝑧 ) = suc ( 𝐶 +o 𝑧 ) )
60 12 59 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( 𝐶 +o suc 𝑧 ) = suc ( 𝐶 +o 𝑧 ) )
61 58 60 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ∩ 𝑆 = suc 𝑧 ) → ( 𝐶 +o ∩ 𝑆 ) = suc ( 𝐶 +o 𝑧 ) )
62 vex ⊢ 𝑧 ∈ V
63 62 sucid ⊢ 𝑧 ∈ suc 𝑧
64 eleq2 ⊢ ( ∩ 𝑆 = suc 𝑧 → ( 𝑧 ∈ ∩ 𝑆 ↔ 𝑧 ∈ suc 𝑧 ) )
65 63 64 mpbiri ⊢ ( ∩ 𝑆 = suc 𝑧 → 𝑧 ∈ ∩ 𝑆 )
66 65 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( ∩ 𝑆 = suc 𝑧 → 𝑧 ∈ ∩ 𝑆 ) )
67 43 eleq2i ⊢ ( 𝑧 ∈ ∩ 𝑆 ↔ 𝑧 ∈ ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } )
68 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐶 +o 𝑦 ) = ( 𝐶 +o 𝑧 ) )
69 68 sseq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) ↔ 𝐷 ⊆ ( 𝐶 +o 𝑧 ) ) )
70 69 onnminsb ⊢ ( 𝑧 ∈ On → ( 𝑧 ∈ ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } → ¬ 𝐷 ⊆ ( 𝐶 +o 𝑧 ) ) )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( 𝑧 ∈ ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } → ¬ 𝐷 ⊆ ( 𝐶 +o 𝑧 ) ) )
72 67 71 biimtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( 𝑧 ∈ ∩ 𝑆 → ¬ 𝐷 ⊆ ( 𝐶 +o 𝑧 ) ) )
73 oacl ⊢ ( ( 𝐶 ∈ On ∧ 𝑧 ∈ On ) → ( 𝐶 +o 𝑧 ) ∈ On )
74 12 73 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( 𝐶 +o 𝑧 ) ∈ On )
75 ontri1 ⊢ ( ( 𝐷 ∈ On ∧ ( 𝐶 +o 𝑧 ) ∈ On ) → ( 𝐷 ⊆ ( 𝐶 +o 𝑧 ) ↔ ¬ ( 𝐶 +o 𝑧 ) ∈ 𝐷 ) )
76 4 74 75 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( 𝐷 ⊆ ( 𝐶 +o 𝑧 ) ↔ ¬ ( 𝐶 +o 𝑧 ) ∈ 𝐷 ) )
77 76 con2bid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( ( 𝐶 +o 𝑧 ) ∈ 𝐷 ↔ ¬ 𝐷 ⊆ ( 𝐶 +o 𝑧 ) ) )
78 72 77 sylibrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( 𝑧 ∈ ∩ 𝑆 → ( 𝐶 +o 𝑧 ) ∈ 𝐷 ) )
79 onsucss ⊢ ( 𝐷 ∈ On → ( ( 𝐶 +o 𝑧 ) ∈ 𝐷 → suc ( 𝐶 +o 𝑧 ) ⊆ 𝐷 ) )
80 4 79 syl ⊢ ( 𝜑 → ( ( 𝐶 +o 𝑧 ) ∈ 𝐷 → suc ( 𝐶 +o 𝑧 ) ⊆ 𝐷 ) )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( ( 𝐶 +o 𝑧 ) ∈ 𝐷 → suc ( 𝐶 +o 𝑧 ) ⊆ 𝐷 ) )
82 66 78 81 3syld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ On ) → ( ∩ 𝑆 = suc 𝑧 → suc ( 𝐶 +o 𝑧 ) ⊆ 𝐷 ) )
83 82 imp ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ∩ 𝑆 = suc 𝑧 ) → suc ( 𝐶 +o 𝑧 ) ⊆ 𝐷 )
84 61 83 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ On ) ∧ ∩ 𝑆 = suc 𝑧 ) → ( 𝐶 +o ∩ 𝑆 ) ⊆ 𝐷 )
85 84 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 → ( 𝐶 +o ∩ 𝑆 ) ⊆ 𝐷 ) )
86 oalim ⊢ ( ( 𝐶 ∈ On ∧ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) → ( 𝐶 +o ∩ 𝑆 ) = ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐶 +o 𝑧 ) )
87 12 86 sylan ⊢ ( ( 𝜑 ∧ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) → ( 𝐶 +o ∩ 𝑆 ) = ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐶 +o 𝑧 ) )
88 onelon ⊢ ( ( ∩ 𝑆 ∈ On ∧ 𝑧 ∈ ∩ 𝑆 ) → 𝑧 ∈ On )
89 19 88 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∩ 𝑆 ) → 𝑧 ∈ On )
90 89 ex ⊢ ( 𝜑 → ( 𝑧 ∈ ∩ 𝑆 → 𝑧 ∈ On ) )
91 90 ancrd ⊢ ( 𝜑 → ( 𝑧 ∈ ∩ 𝑆 → ( 𝑧 ∈ On ∧ 𝑧 ∈ ∩ 𝑆 ) ) )
92 78 expimpd ⊢ ( 𝜑 → ( ( 𝑧 ∈ On ∧ 𝑧 ∈ ∩ 𝑆 ) → ( 𝐶 +o 𝑧 ) ∈ 𝐷 ) )
93 onelss ⊢ ( 𝐷 ∈ On → ( ( 𝐶 +o 𝑧 ) ∈ 𝐷 → ( 𝐶 +o 𝑧 ) ⊆ 𝐷 ) )
94 4 93 syl ⊢ ( 𝜑 → ( ( 𝐶 +o 𝑧 ) ∈ 𝐷 → ( 𝐶 +o 𝑧 ) ⊆ 𝐷 ) )
95 91 92 94 3syld ⊢ ( 𝜑 → ( 𝑧 ∈ ∩ 𝑆 → ( 𝐶 +o 𝑧 ) ⊆ 𝐷 ) )
96 95 ralrimiv ⊢ ( 𝜑 → ∀ 𝑧 ∈ ∩ 𝑆 ( 𝐶 +o 𝑧 ) ⊆ 𝐷 )
97 iunss ⊢ ( ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐶 +o 𝑧 ) ⊆ 𝐷 ↔ ∀ 𝑧 ∈ ∩ 𝑆 ( 𝐶 +o 𝑧 ) ⊆ 𝐷 )
98 96 97 sylibr ⊢ ( 𝜑 → ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐶 +o 𝑧 ) ⊆ 𝐷 )
99 98 adantr ⊢ ( ( 𝜑 ∧ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) → ∪ 𝑧 ∈ ∩ 𝑆 ( 𝐶 +o 𝑧 ) ⊆ 𝐷 )
100 87 99 eqsstrd ⊢ ( ( 𝜑 ∧ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) → ( 𝐶 +o ∩ 𝑆 ) ⊆ 𝐷 )
101 100 ex ⊢ ( 𝜑 → ( ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) → ( 𝐶 +o ∩ 𝑆 ) ⊆ 𝐷 ) )
102 57 85 101 3jaod ⊢ ( 𝜑 → ( ( ∩ 𝑆 = ∅ ∨ ∃ 𝑧 ∈ On ∩ 𝑆 = suc 𝑧 ∨ ( ∩ 𝑆 ∈ V ∧ Lim ∩ 𝑆 ) ) → ( 𝐶 +o ∩ 𝑆 ) ⊆ 𝐷 ) )
103 48 102 mpd ⊢ ( 𝜑 → ( 𝐶 +o ∩ 𝑆 ) ⊆ 𝐷 )
104 10 rspcev ⊢ ( ( 𝐷 ∈ On ∧ 𝐷 ⊆ ( 𝐶 +o 𝐷 ) ) → ∃ 𝑦 ∈ On 𝐷 ⊆ ( 𝐶 +o 𝑦 ) )
105 4 14 104 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ On 𝐷 ⊆ ( 𝐶 +o 𝑦 ) )
106 nfcv ⊢ Ⅎ 𝑦 𝐷
107 nfcv ⊢ Ⅎ 𝑦 𝐶
108 nfcv ⊢ Ⅎ 𝑦 +o
109 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) }
110 109 nfint ⊢ Ⅎ 𝑦 ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) }
111 107 108 110 nfov ⊢ Ⅎ 𝑦 ( 𝐶 +o ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } )
112 106 111 nfss ⊢ Ⅎ 𝑦 𝐷 ⊆ ( 𝐶 +o ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } )
113 oveq2 ⊢ ( 𝑦 = ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } → ( 𝐶 +o 𝑦 ) = ( 𝐶 +o ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } ) )
114 113 sseq2d ⊢ ( 𝑦 = ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } → ( 𝐷 ⊆ ( 𝐶 +o 𝑦 ) ↔ 𝐷 ⊆ ( 𝐶 +o ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } ) ) )
115 112 114 onminsb ⊢ ( ∃ 𝑦 ∈ On 𝐷 ⊆ ( 𝐶 +o 𝑦 ) → 𝐷 ⊆ ( 𝐶 +o ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } ) )
116 105 115 syl ⊢ ( 𝜑 → 𝐷 ⊆ ( 𝐶 +o ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } ) )
117 43 oveq2i ⊢ ( 𝐶 +o ∩ 𝑆 ) = ( 𝐶 +o ∩ { 𝑦 ∈ On ∣ 𝐷 ⊆ ( 𝐶 +o 𝑦 ) } )
118 116 117 sseqtrrdi ⊢ ( 𝜑 → 𝐷 ⊆ ( 𝐶 +o ∩ 𝑆 ) )
119 103 118 eqssd ⊢ ( 𝜑 → ( 𝐶 +o ∩ 𝑆 ) = 𝐷 )
120 omelon ⊢ ω ∈ On
121 omcl ⊢ ( ( ω ∈ On ∧ 𝐷 ∈ On ) → ( ω ·o 𝐷 ) ∈ On )
122 120 4 121 sylancr ⊢ ( 𝜑 → ( ω ·o 𝐷 ) ∈ On )
123 120 a1i ⊢ ( 𝜑 → ω ∈ On )
124 6 5 jca ⊢ ( 𝜑 → ( 𝑁 ∈ 𝑀 ∧ 𝑀 ∈ ω ) )
125 ontr1 ⊢ ( ω ∈ On → ( ( 𝑁 ∈ 𝑀 ∧ 𝑀 ∈ ω ) → 𝑁 ∈ ω ) )
126 123 124 125 sylc ⊢ ( 𝜑 → 𝑁 ∈ ω )
127 nnon ⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
128 126 127 syl ⊢ ( 𝜑 → 𝑁 ∈ On )
129 oaword1 ⊢ ( ( ( ω ·o 𝐷 ) ∈ On ∧ 𝑁 ∈ On ) → ( ω ·o 𝐷 ) ⊆ ( ( ω ·o 𝐷 ) +o 𝑁 ) )
130 122 128 129 syl2anc ⊢ ( 𝜑 → ( ω ·o 𝐷 ) ⊆ ( ( ω ·o 𝐷 ) +o 𝑁 ) )
131 1 oveq1d ⊢ ( 𝜑 → ( 𝐴 +o ( ω ·o ∩ 𝑆 ) ) = ( ( ( ω ·o 𝐶 ) +o 𝑀 ) +o ( ω ·o ∩ 𝑆 ) ) )
132 omcl ⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ) → ( ω ·o 𝐶 ) ∈ On )
133 120 12 132 sylancr ⊢ ( 𝜑 → ( ω ·o 𝐶 ) ∈ On )
134 nnon ⊢ ( 𝑀 ∈ ω → 𝑀 ∈ On )
135 5 134 syl ⊢ ( 𝜑 → 𝑀 ∈ On )
136 omcl ⊢ ( ( ω ∈ On ∧ ∩ 𝑆 ∈ On ) → ( ω ·o ∩ 𝑆 ) ∈ On )
137 120 19 136 sylancr ⊢ ( 𝜑 → ( ω ·o ∩ 𝑆 ) ∈ On )
138 oaass ⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ 𝑀 ∈ On ∧ ( ω ·o ∩ 𝑆 ) ∈ On ) → ( ( ( ω ·o 𝐶 ) +o 𝑀 ) +o ( ω ·o ∩ 𝑆 ) ) = ( ( ω ·o 𝐶 ) +o ( 𝑀 +o ( ω ·o ∩ 𝑆 ) ) ) )
139 133 135 137 138 syl3anc ⊢ ( 𝜑 → ( ( ( ω ·o 𝐶 ) +o 𝑀 ) +o ( ω ·o ∩ 𝑆 ) ) = ( ( ω ·o 𝐶 ) +o ( 𝑀 +o ( ω ·o ∩ 𝑆 ) ) ) )
140 19 120 jctil ⊢ ( 𝜑 → ( ω ∈ On ∧ ∩ 𝑆 ∈ On ) )
141 omword1 ⊢ ( ( ( ω ∈ On ∧ ∩ 𝑆 ∈ On ) ∧ ∅ ∈ ∩ 𝑆 ) → ω ⊆ ( ω ·o ∩ 𝑆 ) )
142 140 44 141 syl2anc ⊢ ( 𝜑 → ω ⊆ ( ω ·o ∩ 𝑆 ) )
143 oaabs ⊢ ( ( ( 𝑀 ∈ ω ∧ ( ω ·o ∩ 𝑆 ) ∈ On ) ∧ ω ⊆ ( ω ·o ∩ 𝑆 ) ) → ( 𝑀 +o ( ω ·o ∩ 𝑆 ) ) = ( ω ·o ∩ 𝑆 ) )
144 5 137 142 143 syl21anc ⊢ ( 𝜑 → ( 𝑀 +o ( ω ·o ∩ 𝑆 ) ) = ( ω ·o ∩ 𝑆 ) )
145 144 oveq2d ⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +o ( 𝑀 +o ( ω ·o ∩ 𝑆 ) ) ) = ( ( ω ·o 𝐶 ) +o ( ω ·o ∩ 𝑆 ) ) )
146 odi ⊢ ( ( ω ∈ On ∧ 𝐶 ∈ On ∧ ∩ 𝑆 ∈ On ) → ( ω ·o ( 𝐶 +o ∩ 𝑆 ) ) = ( ( ω ·o 𝐶 ) +o ( ω ·o ∩ 𝑆 ) ) )
147 123 12 19 146 syl3anc ⊢ ( 𝜑 → ( ω ·o ( 𝐶 +o ∩ 𝑆 ) ) = ( ( ω ·o 𝐶 ) +o ( ω ·o ∩ 𝑆 ) ) )
148 119 oveq2d ⊢ ( 𝜑 → ( ω ·o ( 𝐶 +o ∩ 𝑆 ) ) = ( ω ·o 𝐷 ) )
149 145 147 148 3eqtr2d ⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +o ( 𝑀 +o ( ω ·o ∩ 𝑆 ) ) ) = ( ω ·o 𝐷 ) )
150 131 139 149 3eqtrd ⊢ ( 𝜑 → ( 𝐴 +o ( ω ·o ∩ 𝑆 ) ) = ( ω ·o 𝐷 ) )
151 130 150 2 3sstr4d ⊢ ( 𝜑 → ( 𝐴 +o ( ω ·o ∩ 𝑆 ) ) ⊆ 𝐵 )
152 naddcl ⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ ( ω ·o ∩ 𝑆 ) ∈ On ) → ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) ∈ On )
153 133 137 152 syl2anc ⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) ∈ On )
154 122 153 135 3jca ⊢ ( 𝜑 → ( ( ω ·o 𝐷 ) ∈ On ∧ ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) ∈ On ∧ 𝑀 ∈ On ) )
155 148 147 eqtr3d ⊢ ( 𝜑 → ( ω ·o 𝐷 ) = ( ( ω ·o 𝐶 ) +o ( ω ·o ∩ 𝑆 ) ) )
156 naddgeoa ⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ ( ω ·o ∩ 𝑆 ) ∈ On ) → ( ( ω ·o 𝐶 ) +o ( ω ·o ∩ 𝑆 ) ) ⊆ ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) )
157 133 137 156 syl2anc ⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +o ( ω ·o ∩ 𝑆 ) ) ⊆ ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) )
158 155 157 eqsstrd ⊢ ( 𝜑 → ( ω ·o 𝐷 ) ⊆ ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) )
159 oawordri ⊢ ( ( ( ω ·o 𝐷 ) ∈ On ∧ ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) ∈ On ∧ 𝑀 ∈ On ) → ( ( ω ·o 𝐷 ) ⊆ ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) → ( ( ω ·o 𝐷 ) +o 𝑀 ) ⊆ ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +o 𝑀 ) ) )
160 154 158 159 sylc ⊢ ( 𝜑 → ( ( ω ·o 𝐷 ) +o 𝑀 ) ⊆ ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +o 𝑀 ) )
161 naddonnn ⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ 𝑀 ∈ ω ) → ( ( ω ·o 𝐶 ) +o 𝑀 ) = ( ( ω ·o 𝐶 ) +no 𝑀 ) )
162 133 5 161 syl2anc ⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +o 𝑀 ) = ( ( ω ·o 𝐶 ) +no 𝑀 ) )
163 1 162 eqtrd ⊢ ( 𝜑 → 𝐴 = ( ( ω ·o 𝐶 ) +no 𝑀 ) )
164 163 oveq1d ⊢ ( 𝜑 → ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) = ( ( ( ω ·o 𝐶 ) +no 𝑀 ) +no ( ω ·o ∩ 𝑆 ) ) )
165 naddass ⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ 𝑀 ∈ On ∧ ( ω ·o ∩ 𝑆 ) ∈ On ) → ( ( ( ω ·o 𝐶 ) +no 𝑀 ) +no ( ω ·o ∩ 𝑆 ) ) = ( ( ω ·o 𝐶 ) +no ( 𝑀 +no ( ω ·o ∩ 𝑆 ) ) ) )
166 133 135 137 165 syl3anc ⊢ ( 𝜑 → ( ( ( ω ·o 𝐶 ) +no 𝑀 ) +no ( ω ·o ∩ 𝑆 ) ) = ( ( ω ·o 𝐶 ) +no ( 𝑀 +no ( ω ·o ∩ 𝑆 ) ) ) )
167 naddcom ⊢ ( ( 𝑀 ∈ On ∧ ( ω ·o ∩ 𝑆 ) ∈ On ) → ( 𝑀 +no ( ω ·o ∩ 𝑆 ) ) = ( ( ω ·o ∩ 𝑆 ) +no 𝑀 ) )
168 135 137 167 syl2anc ⊢ ( 𝜑 → ( 𝑀 +no ( ω ·o ∩ 𝑆 ) ) = ( ( ω ·o ∩ 𝑆 ) +no 𝑀 ) )
169 168 oveq2d ⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +no ( 𝑀 +no ( ω ·o ∩ 𝑆 ) ) ) = ( ( ω ·o 𝐶 ) +no ( ( ω ·o ∩ 𝑆 ) +no 𝑀 ) ) )
170 naddonnn ⊢ ( ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) ∈ On ∧ 𝑀 ∈ ω ) → ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +o 𝑀 ) = ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +no 𝑀 ) )
171 153 5 170 syl2anc ⊢ ( 𝜑 → ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +o 𝑀 ) = ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +no 𝑀 ) )
172 naddass ⊢ ( ( ( ω ·o 𝐶 ) ∈ On ∧ ( ω ·o ∩ 𝑆 ) ∈ On ∧ 𝑀 ∈ On ) → ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +no 𝑀 ) = ( ( ω ·o 𝐶 ) +no ( ( ω ·o ∩ 𝑆 ) +no 𝑀 ) ) )
173 133 137 135 172 syl3anc ⊢ ( 𝜑 → ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +no 𝑀 ) = ( ( ω ·o 𝐶 ) +no ( ( ω ·o ∩ 𝑆 ) +no 𝑀 ) ) )
174 171 173 eqtr2d ⊢ ( 𝜑 → ( ( ω ·o 𝐶 ) +no ( ( ω ·o ∩ 𝑆 ) +no 𝑀 ) ) = ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +o 𝑀 ) )
175 166 169 174 3eqtrd ⊢ ( 𝜑 → ( ( ( ω ·o 𝐶 ) +no 𝑀 ) +no ( ω ·o ∩ 𝑆 ) ) = ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +o 𝑀 ) )
176 164 175 eqtr2d ⊢ ( 𝜑 → ( ( ( ω ·o 𝐶 ) +no ( ω ·o ∩ 𝑆 ) ) +o 𝑀 ) = ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) )
177 160 176 sseqtrd ⊢ ( 𝜑 → ( ( ω ·o 𝐷 ) +o 𝑀 ) ⊆ ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) )
178 135 122 jca ⊢ ( 𝜑 → ( 𝑀 ∈ On ∧ ( ω ·o 𝐷 ) ∈ On ) )
179 oaordi ⊢ ( ( 𝑀 ∈ On ∧ ( ω ·o 𝐷 ) ∈ On ) → ( 𝑁 ∈ 𝑀 → ( ( ω ·o 𝐷 ) +o 𝑁 ) ∈ ( ( ω ·o 𝐷 ) +o 𝑀 ) ) )
180 178 6 179 sylc ⊢ ( 𝜑 → ( ( ω ·o 𝐷 ) +o 𝑁 ) ∈ ( ( ω ·o 𝐷 ) +o 𝑀 ) )
181 2 180 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( ω ·o 𝐷 ) +o 𝑀 ) )
182 177 181 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) )
183 119 151 182 3jca ⊢ ( 𝜑 → ( ( 𝐶 +o ∩ 𝑆 ) = 𝐷 ∧ ( 𝐴 +o ( ω ·o ∩ 𝑆 ) ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) ) )
184 oveq2 ⊢ ( 𝑥 = ∩ 𝑆 → ( 𝐶 +o 𝑥 ) = ( 𝐶 +o ∩ 𝑆 ) )
185 184 eqeq1d ⊢ ( 𝑥 = ∩ 𝑆 → ( ( 𝐶 +o 𝑥 ) = 𝐷 ↔ ( 𝐶 +o ∩ 𝑆 ) = 𝐷 ) )
186 oveq2 ⊢ ( 𝑥 = ∩ 𝑆 → ( ω ·o 𝑥 ) = ( ω ·o ∩ 𝑆 ) )
187 186 oveq2d ⊢ ( 𝑥 = ∩ 𝑆 → ( 𝐴 +o ( ω ·o 𝑥 ) ) = ( 𝐴 +o ( ω ·o ∩ 𝑆 ) ) )
188 187 sseq1d ⊢ ( 𝑥 = ∩ 𝑆 → ( ( 𝐴 +o ( ω ·o 𝑥 ) ) ⊆ 𝐵 ↔ ( 𝐴 +o ( ω ·o ∩ 𝑆 ) ) ⊆ 𝐵 ) )
189 186 oveq2d ⊢ ( 𝑥 = ∩ 𝑆 → ( 𝐴 +no ( ω ·o 𝑥 ) ) = ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) )
190 189 eleq2d ⊢ ( 𝑥 = ∩ 𝑆 → ( 𝐵 ∈ ( 𝐴 +no ( ω ·o 𝑥 ) ) ↔ 𝐵 ∈ ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) ) )
191 185 188 190 3anbi123d ⊢ ( 𝑥 = ∩ 𝑆 → ( ( ( 𝐶 +o 𝑥 ) = 𝐷 ∧ ( 𝐴 +o ( ω ·o 𝑥 ) ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +no ( ω ·o 𝑥 ) ) ) ↔ ( ( 𝐶 +o ∩ 𝑆 ) = 𝐷 ∧ ( 𝐴 +o ( ω ·o ∩ 𝑆 ) ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) ) ) )
192 191 rspcev ⊢ ( ( ∩ 𝑆 ∈ ( On ∖ 1o ) ∧ ( ( 𝐶 +o ∩ 𝑆 ) = 𝐷 ∧ ( 𝐴 +o ( ω ·o ∩ 𝑆 ) ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +no ( ω ·o ∩ 𝑆 ) ) ) ) → ∃ 𝑥 ∈ ( On ∖ 1o ) ( ( 𝐶 +o 𝑥 ) = 𝐷 ∧ ( 𝐴 +o ( ω ·o 𝑥 ) ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +no ( ω ·o 𝑥 ) ) ) )
193 46 183 192 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( On ∖ 1o ) ( ( 𝐶 +o 𝑥 ) = 𝐷 ∧ ( 𝐴 +o ( ω ·o 𝑥 ) ) ⊆ 𝐵 ∧ 𝐵 ∈ ( 𝐴 +no ( ω ·o 𝑥 ) ) ) )