Metamath Proof Explorer

Theorem naddle

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

Ref Expression
Assertion naddle ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 +no 𝐵 ) ⊆ 𝐶 ↔ ( ∀ 𝑎 ∈ 𝐴 ( 𝑎 +no 𝐵 ) ∈ 𝐶 ∧ ∀ 𝑏 ∈ 𝐵 ( 𝐴 +no 𝑏 ) ∈ 𝐶 ) ) )

Proof

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