Metamath Proof Explorer

Theorem naddgeoa

Description: Natural addition results in a value greater than or equal than that of ordinal addition. (Contributed by RP, 1-Jan-2025)

Ref Expression
Assertion naddgeoa ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ⊆ A + B

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ a = c → a + 𝑜 b = c + 𝑜 b
2 oveq1 ⊢ a = c → a + b = c + b
3 1 2 sseq12d ⊢ a = c → a + 𝑜 b ⊆ a + b ↔ c + 𝑜 b ⊆ c + b
4 oveq2 ⊢ b = d → c + 𝑜 b = c + 𝑜 d
5 oveq2 ⊢ b = d → c + b = c + d
6 4 5 sseq12d ⊢ b = d → c + 𝑜 b ⊆ c + b ↔ c + 𝑜 d ⊆ c + d
7 oveq1 ⊢ a = c → a + 𝑜 d = c + 𝑜 d
8 oveq1 ⊢ a = c → a + d = c + d
9 7 8 sseq12d ⊢ a = c → a + 𝑜 d ⊆ a + d ↔ c + 𝑜 d ⊆ c + d
10 oveq1 ⊢ a = A → a + 𝑜 b = A + 𝑜 b
11 oveq1 ⊢ a = A → a + b = A + b
12 10 11 sseq12d ⊢ a = A → a + 𝑜 b ⊆ a + b ↔ A + 𝑜 b ⊆ A + b
13 oveq2 ⊢ b = B → A + 𝑜 b = A + 𝑜 B
14 oveq2 ⊢ b = B → A + b = A + B
15 13 14 sseq12d ⊢ b = B → A + 𝑜 b ⊆ A + b ↔ A + 𝑜 B ⊆ A + B
16 simplll ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b ∧ ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a ∈ On
17 simpllr ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b ∧ ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → b ∈ On
18 simplr ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b ∧ ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → Lim ⁡ b
19 17 18 jca ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b ∧ ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → b ∈ On ∧ Lim ⁡ b
20 oalim ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b → a + 𝑜 b = ⋃ d ∈ b a + 𝑜 d
21 16 19 20 syl2anc ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b ∧ ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b = ⋃ d ∈ b a + 𝑜 d
22 simpl ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b → a ∈ On ∧ b ∈ On
23 simp3 ⊢ ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → ∀ d ∈ b a + 𝑜 d ⊆ a + d
24 simpr ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 d ⊆ a + d
25 simpr ⊢ a ∈ On ∧ b ∈ On → b ∈ On
26 onelss ⊢ b ∈ On → d ∈ b → d ⊆ b
27 25 26 syl ⊢ a ∈ On ∧ b ∈ On → d ∈ b → d ⊆ b
28 27 imp ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → d ⊆ b
29 simplr ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → b ∈ On
30 simpr ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → d ∈ b
31 onelon ⊢ b ∈ On ∧ d ∈ b → d ∈ On
32 29 30 31 syl2anc ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → d ∈ On
33 simpll ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → a ∈ On
34 naddss2 ⊢ d ∈ On ∧ b ∈ On ∧ a ∈ On → d ⊆ b ↔ a + d ⊆ a + b
35 32 29 33 34 syl3anc ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → d ⊆ b ↔ a + d ⊆ a + b
36 28 35 mpbid ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → a + d ⊆ a + b
37 36 adantr ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ a + 𝑜 d ⊆ a + d → a + d ⊆ a + b
38 24 37 sstrd ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 d ⊆ a + b
39 38 ex ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → a + 𝑜 d ⊆ a + d → a + 𝑜 d ⊆ a + b
40 39 ralimdva ⊢ a ∈ On ∧ b ∈ On → ∀ d ∈ b a + 𝑜 d ⊆ a + d → ∀ d ∈ b a + 𝑜 d ⊆ a + b
41 40 imp ⊢ a ∈ On ∧ b ∈ On ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → ∀ d ∈ b a + 𝑜 d ⊆ a + b
42 iunss ⊢ ⋃ d ∈ b a + 𝑜 d ⊆ a + b ↔ ∀ d ∈ b a + 𝑜 d ⊆ a + b
43 41 42 sylibr ⊢ a ∈ On ∧ b ∈ On ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → ⋃ d ∈ b a + 𝑜 d ⊆ a + b
44 22 23 43 syl2an ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b ∧ ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → ⋃ d ∈ b a + 𝑜 d ⊆ a + b
45 21 44 eqsstrd ⊢ a ∈ On ∧ b ∈ On ∧ Lim ⁡ b ∧ ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
46 45 exp31 ⊢ a ∈ On ∧ b ∈ On → Lim ⁡ b → ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
47 dflim3 ⊢ Lim ⁡ b ↔ Ord ⁡ b ∧ ¬ b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d
48 47 notbii ⊢ ¬ Lim ⁡ b ↔ ¬ Ord ⁡ b ∧ ¬ b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d
49 iman ⊢ Ord ⁡ b → b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d ↔ ¬ Ord ⁡ b ∧ ¬ b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d
50 48 49 bitr4i ⊢ ¬ Lim ⁡ b ↔ Ord ⁡ b → b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d
51 eloni ⊢ b ∈ On → Ord ⁡ b
52 pm5.5 ⊢ Ord ⁡ b → Ord ⁡ b → b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d ↔ b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d
53 25 51 52 3syl ⊢ a ∈ On ∧ b ∈ On → Ord ⁡ b → b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d ↔ b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d
54 50 53 bitrid ⊢ a ∈ On ∧ b ∈ On → ¬ Lim ⁡ b ↔ b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d
55 ssidd ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a ⊆ a
56 simpr ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → b = ∅
57 56 oveq2d ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a + 𝑜 b = a + 𝑜 ∅
58 simpll ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a ∈ On
59 oa0 ⊢ a ∈ On → a + 𝑜 ∅ = a
60 58 59 syl ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a + 𝑜 ∅ = a
61 57 60 eqtrd ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a + 𝑜 b = a
62 56 oveq2d ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a + b = a + ∅
63 naddrid ⊢ a ∈ On → a + ∅ = a
64 58 63 syl ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a + ∅ = a
65 62 64 eqtrd ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a + b = a
66 55 61 65 3sstr4d ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → a + 𝑜 b ⊆ a + b
67 66 a1d ⊢ a ∈ On ∧ b ∈ On ∧ b = ∅ → ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
68 67 ex ⊢ a ∈ On ∧ b ∈ On → b = ∅ → ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
69 vex ⊢ d ∈ V
70 69 sucid ⊢ d ∈ suc ⁡ d
71 simpr ⊢ d ∈ On ∧ b = suc ⁡ d → b = suc ⁡ d
72 70 71 eleqtrrid ⊢ d ∈ On ∧ b = suc ⁡ d → d ∈ b
73 72 71 jca ⊢ d ∈ On ∧ b = suc ⁡ d → d ∈ b ∧ b = suc ⁡ d
74 73 a1i ⊢ a ∈ On ∧ b ∈ On → d ∈ On ∧ b = suc ⁡ d → d ∈ b ∧ b = suc ⁡ d
75 74 reximdv2 ⊢ a ∈ On ∧ b ∈ On → ∃ d ∈ On b = suc ⁡ d → ∃ d ∈ b b = suc ⁡ d
76 r19.29r ⊢ ∃ d ∈ b b = suc ⁡ d ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → ∃ d ∈ b b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d
77 simprr ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 d ⊆ a + d
78 33 32 jca ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → a ∈ On ∧ d ∈ On
79 oacl ⊢ a ∈ On ∧ d ∈ On → a + 𝑜 d ∈ On
80 eloni ⊢ a + 𝑜 d ∈ On → Ord ⁡ a + 𝑜 d
81 79 80 syl ⊢ a ∈ On ∧ d ∈ On → Ord ⁡ a + 𝑜 d
82 naddcl ⊢ a ∈ On ∧ d ∈ On → a + d ∈ On
83 eloni ⊢ a + d ∈ On → Ord ⁡ a + d
84 82 83 syl ⊢ a ∈ On ∧ d ∈ On → Ord ⁡ a + d
85 81 84 jca ⊢ a ∈ On ∧ d ∈ On → Ord ⁡ a + 𝑜 d ∧ Ord ⁡ a + d
86 ordsucsssuc ⊢ Ord ⁡ a + 𝑜 d ∧ Ord ⁡ a + d → a + 𝑜 d ⊆ a + d ↔ suc ⁡ a + 𝑜 d ⊆ suc ⁡ a + d
87 78 85 86 3syl ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b → a + 𝑜 d ⊆ a + d ↔ suc ⁡ a + 𝑜 d ⊆ suc ⁡ a + d
88 87 adantr ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 d ⊆ a + d ↔ suc ⁡ a + 𝑜 d ⊆ suc ⁡ a + d
89 77 88 mpbid ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → suc ⁡ a + 𝑜 d ⊆ suc ⁡ a + d
90 simprl ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → b = suc ⁡ d
91 90 oveq2d ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 b = a + 𝑜 suc ⁡ d
92 78 adantr ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a ∈ On ∧ d ∈ On
93 oasuc ⊢ a ∈ On ∧ d ∈ On → a + 𝑜 suc ⁡ d = suc ⁡ a + 𝑜 d
94 92 93 syl ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 suc ⁡ d = suc ⁡ a + 𝑜 d
95 91 94 eqtrd ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 b = suc ⁡ a + 𝑜 d
96 90 oveq2d ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + b = a + suc ⁡ d
97 simplll ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a ∈ On
98 31 ad4ant23 ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → d ∈ On
99 naddsuc2 ⊢ a ∈ On ∧ d ∈ On → a + suc ⁡ d = suc ⁡ a + d
100 97 98 99 syl2anc ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + suc ⁡ d = suc ⁡ a + d
101 96 100 eqtrd ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + b = suc ⁡ a + d
102 89 95 101 3sstr4d ⊢ a ∈ On ∧ b ∈ On ∧ d ∈ b ∧ b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
103 102 rexlimdva2 ⊢ a ∈ On ∧ b ∈ On → ∃ d ∈ b b = suc ⁡ d ∧ a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
104 76 103 syl5 ⊢ a ∈ On ∧ b ∈ On → ∃ d ∈ b b = suc ⁡ d ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
105 104 expd ⊢ a ∈ On ∧ b ∈ On → ∃ d ∈ b b = suc ⁡ d → ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
106 23 105 syl7 ⊢ a ∈ On ∧ b ∈ On → ∃ d ∈ b b = suc ⁡ d → ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
107 75 106 syld ⊢ a ∈ On ∧ b ∈ On → ∃ d ∈ On b = suc ⁡ d → ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
108 68 107 jaod ⊢ a ∈ On ∧ b ∈ On → b = ∅ ∨ ∃ d ∈ On b = suc ⁡ d → ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
109 54 108 sylbid ⊢ a ∈ On ∧ b ∈ On → ¬ Lim ⁡ b → ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
110 46 109 pm2.61d ⊢ a ∈ On ∧ b ∈ On → ∀ c ∈ a ∀ d ∈ b c + 𝑜 d ⊆ c + d ∧ ∀ c ∈ a c + 𝑜 b ⊆ c + b ∧ ∀ d ∈ b a + 𝑜 d ⊆ a + d → a + 𝑜 b ⊆ a + b
111 3 6 9 12 15 110 on2ind ⊢ A ∈ On ∧ B ∈ On → A + 𝑜 B ⊆ A + B