Metamath Proof Explorer

Theorem naddasslem1

Description: Lemma for naddass . Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Assertion naddasslem1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B + C = ⋂ x ∈ On | ∀ a ∈ A a + B + C ∈ x ∧ ∀ b ∈ B A + b + C ∈ x ∧ ∀ c ∈ C A + B + c ∈ x

Proof

Step Hyp Ref Expression
1 naddcl ⊢ A ∈ On ∧ B ∈ On → A + B ∈ On
2 1 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B ∈ On
3 simp3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ∈ On
4 naddov3 ⊢ A ∈ On ∧ B ∈ On → A + B = ⋂ a ∈ On | + A × B ∪ + A × B ⊆ a
5 4 3adant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B = ⋂ a ∈ On | + A × B ∪ + A × B ⊆ a
6 intmin ⊢ C ∈ On → ⋂ c ∈ On | C ⊆ c = C
7 6 eqcomd ⊢ C ∈ On → C = ⋂ c ∈ On | C ⊆ c
8 7 3ad2ant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C = ⋂ c ∈ On | C ⊆ c
9 2 3 5 8 naddunif ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B + C = ⋂ x ∈ On | + + A × B ∪ + A × B × C ∪ + A + B × C ⊆ x
10 df-3an ⊢ + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x ∧ + A + B × C ⊆ x ↔ + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x ∧ + A + B × C ⊆ x
11 unss ⊢ + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x ↔ + + A × B × C ∪ + + A × B × C ⊆ x
12 ancom ⊢ + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x ↔ + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x
13 xpundir ⊢ + A × B ∪ + A × B × C = + A × B × C ∪ + A × B × C
14 13 imaeq2i ⊢ + + A × B ∪ + A × B × C = + + A × B × C ∪ + A × B × C
15 imaundi ⊢ + + A × B × C ∪ + A × B × C = + + A × B × C ∪ + + A × B × C
16 14 15 eqtri ⊢ + + A × B ∪ + A × B × C = + + A × B × C ∪ + + A × B × C
17 16 sseq1i ⊢ + + A × B ∪ + A × B × C ⊆ x ↔ + + A × B × C ∪ + + A × B × C ⊆ x
18 11 12 17 3bitr4i ⊢ + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x ↔ + + A × B ∪ + A × B × C ⊆ x
19 18 anbi1i ⊢ + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x ∧ + A + B × C ⊆ x ↔ + + A × B ∪ + A × B × C ⊆ x ∧ + A + B × C ⊆ x
20 unss ⊢ + + A × B ∪ + A × B × C ⊆ x ∧ + A + B × C ⊆ x ↔ + + A × B ∪ + A × B × C ∪ + A + B × C ⊆ x
21 10 19 20 3bitrri ⊢ + + A × B ∪ + A × B × C ∪ + A + B × C ⊆ x ↔ + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x ∧ + A + B × C ⊆ x
22 naddfn ⊢ + Fn On × On
23 fnfun ⊢ + Fn On × On → Fun ⁡ +
24 22 23 ax-mp ⊢ Fun ⁡ +
25 imassrn ⊢ + A × B ⊆ ran ⁡ +
26 naddf ⊢ + : On × On ⟶ On
27 frn ⊢ + : On × On ⟶ On → ran ⁡ + ⊆ On
28 26 27 ax-mp ⊢ ran ⁡ + ⊆ On
29 25 28 sstri ⊢ + A × B ⊆ On
30 simpl3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → C ∈ On
31 30 snssd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → C ⊆ On
32 xpss12 ⊢ + A × B ⊆ On ∧ C ⊆ On → + A × B × C ⊆ On × On
33 29 31 32 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × B × C ⊆ On × On
34 22 fndmi ⊢ dom ⁡ + = On × On
35 33 34 sseqtrrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × B × C ⊆ dom ⁡ +
36 funimassov ⊢ Fun ⁡ + ∧ + A × B × C ⊆ dom ⁡ + → + + A × B × C ⊆ x ↔ ∀ p ∈ + A × B ∀ c ∈ C p + c ∈ x
37 24 35 36 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + + A × B × C ⊆ x ↔ ∀ p ∈ + A × B ∀ c ∈ C p + c ∈ x
38 oveq2 ⊢ c = C → p + c = p + C
39 38 eleq1d ⊢ c = C → p + c ∈ x ↔ p + C ∈ x
40 39 ralsng ⊢ C ∈ On → ∀ c ∈ C p + c ∈ x ↔ p + C ∈ x
41 30 40 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ c ∈ C p + c ∈ x ↔ p + C ∈ x
42 41 ralbidv ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + A × B ∀ c ∈ C p + c ∈ x ↔ ∀ p ∈ + A × B p + C ∈ x
43 onss ⊢ A ∈ On → A ⊆ On
44 43 3ad2ant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ On
45 44 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A ⊆ On
46 simpl2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B ∈ On
47 46 snssd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B ⊆ On
48 xpss12 ⊢ A ⊆ On ∧ B ⊆ On → A × B ⊆ On × On
49 45 47 48 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A × B ⊆ On × On
50 oveq1 ⊢ p = a + b → p + C = a + b + C
51 50 eleq1d ⊢ p = a + b → p + C ∈ x ↔ a + b + C ∈ x
52 51 imaeqalov ⊢ + Fn On × On ∧ A × B ⊆ On × On → ∀ p ∈ + A × B p + C ∈ x ↔ ∀ a ∈ A ∀ b ∈ B a + b + C ∈ x
53 22 49 52 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + A × B p + C ∈ x ↔ ∀ a ∈ A ∀ b ∈ B a + b + C ∈ x
54 oveq2 ⊢ b = B → a + b = a + B
55 54 oveq1d ⊢ b = B → a + b + C = a + B + C
56 55 eleq1d ⊢ b = B → a + b + C ∈ x ↔ a + B + C ∈ x
57 56 ralsng ⊢ B ∈ On → ∀ b ∈ B a + b + C ∈ x ↔ a + B + C ∈ x
58 46 57 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ b ∈ B a + b + C ∈ x ↔ a + B + C ∈ x
59 58 ralbidv ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ a ∈ A ∀ b ∈ B a + b + C ∈ x ↔ ∀ a ∈ A a + B + C ∈ x
60 53 59 bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + A × B p + C ∈ x ↔ ∀ a ∈ A a + B + C ∈ x
61 37 42 60 3bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + + A × B × C ⊆ x ↔ ∀ a ∈ A a + B + C ∈ x
62 imassrn ⊢ + A × B ⊆ ran ⁡ +
63 62 28 sstri ⊢ + A × B ⊆ On
64 xpss12 ⊢ + A × B ⊆ On ∧ C ⊆ On → + A × B × C ⊆ On × On
65 63 31 64 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × B × C ⊆ On × On
66 65 34 sseqtrrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × B × C ⊆ dom ⁡ +
67 funimassov ⊢ Fun ⁡ + ∧ + A × B × C ⊆ dom ⁡ + → + + A × B × C ⊆ x ↔ ∀ p ∈ + A × B ∀ c ∈ C p + c ∈ x
68 24 66 67 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + + A × B × C ⊆ x ↔ ∀ p ∈ + A × B ∀ c ∈ C p + c ∈ x
69 41 ralbidv ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + A × B ∀ c ∈ C p + c ∈ x ↔ ∀ p ∈ + A × B p + C ∈ x
70 simpl1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A ∈ On
71 70 snssd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A ⊆ On
72 onss ⊢ B ∈ On → B ⊆ On
73 72 3ad2ant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ⊆ On
74 73 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B ⊆ On
75 xpss12 ⊢ A ⊆ On ∧ B ⊆ On → A × B ⊆ On × On
76 71 74 75 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A × B ⊆ On × On
77 51 imaeqalov ⊢ + Fn On × On ∧ A × B ⊆ On × On → ∀ p ∈ + A × B p + C ∈ x ↔ ∀ a ∈ A ∀ b ∈ B a + b + C ∈ x
78 22 76 77 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + A × B p + C ∈ x ↔ ∀ a ∈ A ∀ b ∈ B a + b + C ∈ x
79 oveq1 ⊢ a = A → a + b = A + b
80 79 oveq1d ⊢ a = A → a + b + C = A + b + C
81 80 eleq1d ⊢ a = A → a + b + C ∈ x ↔ A + b + C ∈ x
82 81 ralbidv ⊢ a = A → ∀ b ∈ B a + b + C ∈ x ↔ ∀ b ∈ B A + b + C ∈ x
83 82 ralsng ⊢ A ∈ On → ∀ a ∈ A ∀ b ∈ B a + b + C ∈ x ↔ ∀ b ∈ B A + b + C ∈ x
84 70 83 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ a ∈ A ∀ b ∈ B a + b + C ∈ x ↔ ∀ b ∈ B A + b + C ∈ x
85 78 84 bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + A × B p + C ∈ x ↔ ∀ b ∈ B A + b + C ∈ x
86 68 69 85 3bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + + A × B × C ⊆ x ↔ ∀ b ∈ B A + b + C ∈ x
87 2 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A + B ∈ On
88 87 snssd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A + B ⊆ On
89 onss ⊢ C ∈ On → C ⊆ On
90 89 3ad2ant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⊆ On
91 90 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → C ⊆ On
92 xpss12 ⊢ A + B ⊆ On ∧ C ⊆ On → A + B × C ⊆ On × On
93 88 91 92 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A + B × C ⊆ On × On
94 93 34 sseqtrrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A + B × C ⊆ dom ⁡ +
95 funimassov ⊢ Fun ⁡ + ∧ A + B × C ⊆ dom ⁡ + → + A + B × C ⊆ x ↔ ∀ a ∈ A + B ∀ c ∈ C a + c ∈ x
96 24 94 95 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A + B × C ⊆ x ↔ ∀ a ∈ A + B ∀ c ∈ C a + c ∈ x
97 ovex ⊢ A + B ∈ V
98 oveq1 ⊢ a = A + B → a + c = A + B + c
99 98 eleq1d ⊢ a = A + B → a + c ∈ x ↔ A + B + c ∈ x
100 99 ralbidv ⊢ a = A + B → ∀ c ∈ C a + c ∈ x ↔ ∀ c ∈ C A + B + c ∈ x
101 97 100 ralsn ⊢ ∀ a ∈ A + B ∀ c ∈ C a + c ∈ x ↔ ∀ c ∈ C A + B + c ∈ x
102 96 101 bitrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A + B × C ⊆ x ↔ ∀ c ∈ C A + B + c ∈ x
103 61 86 102 3anbi123d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + + A × B × C ⊆ x ∧ + + A × B × C ⊆ x ∧ + A + B × C ⊆ x ↔ ∀ a ∈ A a + B + C ∈ x ∧ ∀ b ∈ B A + b + C ∈ x ∧ ∀ c ∈ C A + B + c ∈ x
104 21 103 bitrid ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + + A × B ∪ + A × B × C ∪ + A + B × C ⊆ x ↔ ∀ a ∈ A a + B + C ∈ x ∧ ∀ b ∈ B A + b + C ∈ x ∧ ∀ c ∈ C A + B + c ∈ x
105 104 rabbidva ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → x ∈ On | + + A × B ∪ + A × B × C ∪ + A + B × C ⊆ x = x ∈ On | ∀ a ∈ A a + B + C ∈ x ∧ ∀ b ∈ B A + b + C ∈ x ∧ ∀ c ∈ C A + B + c ∈ x
106 105 inteqd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → ⋂ x ∈ On | + + A × B ∪ + A × B × C ∪ + A + B × C ⊆ x = ⋂ x ∈ On | ∀ a ∈ A a + B + C ∈ x ∧ ∀ b ∈ B A + b + C ∈ x ∧ ∀ c ∈ C A + B + c ∈ x
107 9 106 eqtrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B + C = ⋂ x ∈ On | ∀ a ∈ A a + B + C ∈ x ∧ ∀ b ∈ B A + b + C ∈ x ∧ ∀ c ∈ C A + B + c ∈ x