Metamath Proof Explorer

Theorem ltnadd

Description: Condition for bounding a natural sum below. (Contributed by Scott Fenton, 21-Jul-2026)

Ref Expression
Assertion ltnadd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B + C ↔ ∃ b ∈ B A ⊆ b + C ∨ ∃ c ∈ C A ⊆ B + c

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ x = A → B + c ∈ x ↔ B + c ∈ A
2 1 ralbidv ⊢ x = A → ∀ c ∈ C B + c ∈ x ↔ ∀ c ∈ C B + c ∈ A
3 eleq2 ⊢ x = A → b + C ∈ x ↔ b + C ∈ A
4 3 ralbidv ⊢ x = A → ∀ b ∈ B b + C ∈ x ↔ ∀ b ∈ B b + C ∈ A
5 2 4 anbi12d ⊢ x = A → ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x ↔ ∀ c ∈ C B + c ∈ A ∧ ∀ b ∈ B b + C ∈ A
6 5 onnminsb ⊢ A ∈ On → A ∈ ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x → ¬ ∀ c ∈ C B + c ∈ A ∧ ∀ b ∈ B b + C ∈ A
7 6 3ad2ant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x → ¬ ∀ c ∈ C B + c ∈ A ∧ ∀ b ∈ B b + C ∈ A
8 naddov2 ⊢ B ∈ On ∧ C ∈ On → B + C = ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x
9 8 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C = ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x
10 9 eleq2d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B + C ↔ A ∈ ⋂ x ∈ On | ∀ c ∈ C B + c ∈ x ∧ ∀ b ∈ B b + C ∈ x
11 simpl1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → A ∈ On
12 onss ⊢ B ∈ On → B ⊆ On
13 12 3ad2ant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ⊆ On
14 13 sselda ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → b ∈ On
15 simpl3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → C ∈ On
16 14 15 naddcld ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → b + C ∈ On
17 ontri1 ⊢ A ∈ On ∧ b + C ∈ On → A ⊆ b + C ↔ ¬ b + C ∈ A
18 11 16 17 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B → A ⊆ b + C ↔ ¬ b + C ∈ A
19 18 rexbidva ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ b ∈ B A ⊆ b + C ↔ ∃ b ∈ B ¬ b + C ∈ A
20 simpl1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C → A ∈ On
21 simpl2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C → B ∈ On
22 onss ⊢ C ∈ On → C ⊆ On
23 22 3ad2ant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⊆ On
24 23 sselda ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C → c ∈ On
25 21 24 naddcld ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C → B + c ∈ On
26 ontri1 ⊢ A ∈ On ∧ B + c ∈ On → A ⊆ B + c ↔ ¬ B + c ∈ A
27 20 25 26 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C → A ⊆ B + c ↔ ¬ B + c ∈ A
28 27 rexbidva ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ c ∈ C A ⊆ B + c ↔ ∃ c ∈ C ¬ B + c ∈ A
29 19 28 orbi12d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ b ∈ B A ⊆ b + C ∨ ∃ c ∈ C A ⊆ B + c ↔ ∃ b ∈ B ¬ b + C ∈ A ∨ ∃ c ∈ C ¬ B + c ∈ A
30 orcom ⊢ ¬ ∀ b ∈ B b + C ∈ A ∨ ¬ ∀ c ∈ C B + c ∈ A ↔ ¬ ∀ c ∈ C B + c ∈ A ∨ ¬ ∀ b ∈ B b + C ∈ A
31 rexnal ⊢ ∃ b ∈ B ¬ b + C ∈ A ↔ ¬ ∀ b ∈ B b + C ∈ A
32 rexnal ⊢ ∃ c ∈ C ¬ B + c ∈ A ↔ ¬ ∀ c ∈ C B + c ∈ A
33 31 32 orbi12i ⊢ ∃ b ∈ B ¬ b + C ∈ A ∨ ∃ c ∈ C ¬ B + c ∈ A ↔ ¬ ∀ b ∈ B b + C ∈ A ∨ ¬ ∀ c ∈ C B + c ∈ A
34 ianor ⊢ ¬ ∀ c ∈ C B + c ∈ A ∧ ∀ b ∈ B b + C ∈ A ↔ ¬ ∀ c ∈ C B + c ∈ A ∨ ¬ ∀ b ∈ B b + C ∈ A
35 30 33 34 3bitr4i ⊢ ∃ b ∈ B ¬ b + C ∈ A ∨ ∃ c ∈ C ¬ B + c ∈ A ↔ ¬ ∀ c ∈ C B + c ∈ A ∧ ∀ b ∈ B b + C ∈ A
36 29 35 bitrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ b ∈ B A ⊆ b + C ∨ ∃ c ∈ C A ⊆ B + c ↔ ¬ ∀ c ∈ C B + c ∈ A ∧ ∀ b ∈ B b + C ∈ A
37 7 10 36 3imtr4d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B + C → ∃ b ∈ B A ⊆ b + C ∨ ∃ c ∈ C A ⊆ B + c
38 simprr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → A ⊆ b + C
39 simprl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → b ∈ B
40 14 adantrr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → b ∈ On
41 simpl2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → B ∈ On
42 simpl3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → C ∈ On
43 naddel1 ⊢ b ∈ On ∧ B ∈ On ∧ C ∈ On → b ∈ B ↔ b + C ∈ B + C
44 40 41 42 43 syl3anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → b ∈ B ↔ b + C ∈ B + C
45 39 44 mpbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → b + C ∈ B + C
46 simpl1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → A ∈ On
47 naddcl ⊢ B ∈ On ∧ C ∈ On → B + C ∈ On
48 47 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C ∈ On
49 48 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → B + C ∈ On
50 ontr2 ⊢ A ∈ On ∧ B + C ∈ On → A ⊆ b + C ∧ b + C ∈ B + C → A ∈ B + C
51 46 49 50 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → A ⊆ b + C ∧ b + C ∈ B + C → A ∈ B + C
52 38 45 51 mp2and ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ b ∈ B ∧ A ⊆ b + C → A ∈ B + C
53 52 rexlimdvaa ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ b ∈ B A ⊆ b + C → A ∈ B + C
54 simprr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → A ⊆ B + c
55 simprl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → c ∈ C
56 24 adantrr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → c ∈ On
57 simpl3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → C ∈ On
58 simpl2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → B ∈ On
59 naddel2 ⊢ c ∈ On ∧ C ∈ On ∧ B ∈ On → c ∈ C ↔ B + c ∈ B + C
60 56 57 58 59 syl3anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → c ∈ C ↔ B + c ∈ B + C
61 55 60 mpbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → B + c ∈ B + C
62 simpl1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → A ∈ On
63 48 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → B + C ∈ On
64 ontr2 ⊢ A ∈ On ∧ B + C ∈ On → A ⊆ B + c ∧ B + c ∈ B + C → A ∈ B + C
65 62 63 64 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → A ⊆ B + c ∧ B + c ∈ B + C → A ∈ B + C
66 54 61 65 mp2and ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ c ∈ C ∧ A ⊆ B + c → A ∈ B + C
67 66 rexlimdvaa ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ c ∈ C A ⊆ B + c → A ∈ B + C
68 53 67 jaod ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ∃ b ∈ B A ⊆ b + C ∨ ∃ c ∈ C A ⊆ B + c → A ∈ B + C
69 37 68 impbid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ B + C ↔ ∃ b ∈ B A ⊆ b + C ∨ ∃ c ∈ C A ⊆ B + c