Metamath Proof Explorer

Theorem naddle

Description: Condition for bounding natural addition above. (Contributed by Scott Fenton, 21-Jul-2026)

Ref Expression
Assertion naddle ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B ⊆ C ↔ ∀ a ∈ A a + B ∈ C ∧ ∀ b ∈ B A + b ∈ C

Proof

Step Hyp Ref Expression
1 ltnadd ⊢ C ∈ On ∧ A ∈ On ∧ B ∈ On → C ∈ A + B ↔ ∃ a ∈ A C ⊆ a + B ∨ ∃ b ∈ B C ⊆ A + b
2 1 3coml ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ∈ A + B ↔ ∃ a ∈ A C ⊆ a + B ∨ ∃ b ∈ B C ⊆ A + b
3 2 notbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ¬ C ∈ A + B ↔ ¬ ∃ a ∈ A C ⊆ a + B ∨ ∃ b ∈ B C ⊆ A + b
4 naddcl ⊢ A ∈ On ∧ B ∈ On → A + B ∈ On
5 4 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B ∈ On
6 simp3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ∈ On
7 ontri1 ⊢ A + B ∈ On ∧ C ∈ On → A + B ⊆ C ↔ ¬ C ∈ A + B
8 5 6 7 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B ⊆ C ↔ ¬ C ∈ A + B
9 simpl3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ a ∈ A → C ∈ On
10 onss ⊢ A ∈ On → A ⊆ On
11 10 3ad2ant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ On
12 11 sselda ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ a ∈ A → a ∈ On
13 simpl2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ a ∈ A → B ∈ On
14 12 13 naddcld ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ a ∈ A → a + B ∈ On
15 ontri1 ⊢ C ∈ On ∧ a + B ∈ On → C ⊆ a + B ↔ ¬ a + B ∈ C
16 9 14 15 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ a ∈ A → C ⊆ a + B ↔ ¬ a + B ∈ C
17 16 rexbidva ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ a ∈ A C ⊆ a + B ↔ ∃ a ∈ A ¬ a + B ∈ C
18 simpl3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → C ∈ On
19 simpl1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → A ∈ On
20 onss ⊢ B ∈ On → B ⊆ On
21 20 3ad2ant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ⊆ On
22 21 sselda ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → b ∈ On
23 19 22 naddcld ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → A + b ∈ On
24 ontri1 ⊢ C ∈ On ∧ A + b ∈ On → C ⊆ A + b ↔ ¬ A + b ∈ C
25 18 23 24 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → C ⊆ A + b ↔ ¬ A + b ∈ C
26 25 rexbidva ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ b ∈ B C ⊆ A + b ↔ ∃ b ∈ B ¬ A + b ∈ C
27 17 26 orbi12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ a ∈ A C ⊆ a + B ∨ ∃ b ∈ B C ⊆ A + b ↔ ∃ a ∈ A ¬ a + B ∈ C ∨ ∃ b ∈ B ¬ A + b ∈ C
28 rexnal ⊢ ∃ a ∈ A ¬ a + B ∈ C ↔ ¬ ∀ a ∈ A a + B ∈ C
29 rexnal ⊢ ∃ b ∈ B ¬ A + b ∈ C ↔ ¬ ∀ b ∈ B A + b ∈ C
30 28 29 orbi12i ⊢ ∃ a ∈ A ¬ a + B ∈ C ∨ ∃ b ∈ B ¬ A + b ∈ C ↔ ¬ ∀ a ∈ A a + B ∈ C ∨ ¬ ∀ b ∈ B A + b ∈ C
31 ianor ⊢ ¬ ∀ a ∈ A a + B ∈ C ∧ ∀ b ∈ B A + b ∈ C ↔ ¬ ∀ a ∈ A a + B ∈ C ∨ ¬ ∀ b ∈ B A + b ∈ C
32 30 31 bitr4i ⊢ ∃ a ∈ A ¬ a + B ∈ C ∨ ∃ b ∈ B ¬ A + b ∈ C ↔ ¬ ∀ a ∈ A a + B ∈ C ∧ ∀ b ∈ B A + b ∈ C
33 27 32 bitrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ a ∈ A C ⊆ a + B ∨ ∃ b ∈ B C ⊆ A + b ↔ ¬ ∀ a ∈ A a + B ∈ C ∧ ∀ b ∈ B A + b ∈ C
34 33 con2bid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∀ a ∈ A a + B ∈ C ∧ ∀ b ∈ B A + b ∈ C ↔ ¬ ∃ a ∈ A C ⊆ a + B ∨ ∃ b ∈ B C ⊆ A + b
35 3 8 34 3bitr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B ⊆ C ↔ ∀ a ∈ A a + B ∈ C ∧ ∀ b ∈ B A + b ∈ C