Metamath Proof Explorer

Theorem naddasslem2

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

Ref Expression
Assertion naddasslem2 ⊢ 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 simp1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ∈ On
2 naddcl ⊢ B ∈ On ∧ C ∈ On → B + C ∈ On
3 2 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C ∈ On
4 intmin ⊢ A ∈ On → ⋂ a ∈ On | A ⊆ a = A
5 4 eqcomd ⊢ A ∈ On → A = ⋂ a ∈ On | A ⊆ a
6 5 3ad2ant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A = ⋂ a ∈ On | A ⊆ a
7 naddov3 ⊢ B ∈ On ∧ C ∈ On → B + C = ⋂ p ∈ On | + B × C ∪ + B × C ⊆ p
8 7 3adant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B + C = ⋂ p ∈ On | + B × C ∪ + B × C ⊆ p
9 1 3 6 8 naddunif ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B + C = ⋂ x ∈ On | + A × B + C ∪ + A × + B × C ∪ + B × C ⊆ x
10 3anass ⊢ + 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 xpundi ⊢ A × + B × C ∪ + B × C = A × + B × C ∪ A × + B × C
14 13 imaeq2i ⊢ + A × + B × C ∪ + 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 × C ∪ + B × C = + A × + B × C ∪ + A × + B × C
17 16 sseq1i ⊢ + A × + B × C ∪ + 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 × C ∪ + B × C ⊆ x
19 18 anbi2i ⊢ + A × B + C ⊆ x ∧ + A × + B × C ⊆ x ∧ + A × + B × C ⊆ x ↔ + A × B + C ⊆ x ∧ + A × + B × C ∪ + B × C ⊆ x
20 unss ⊢ + A × B + C ⊆ x ∧ + A × + B × C ∪ + B × C ⊆ x ↔ + A × B + C ∪ + A × + B × C ∪ + B × C ⊆ x
21 10 19 20 3bitrri ⊢ + A × B + C ∪ + A × + B × C ∪ + 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 onss ⊢ A ∈ On → A ⊆ On
26 25 3ad2ant1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A ⊆ On
27 3 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B + C ∈ On
28 27 snssd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B + C ⊆ On
29 xpss12 ⊢ A ⊆ On ∧ B + C ⊆ On → A × B + C ⊆ On × On
30 26 28 29 syl2an2r ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A × B + C ⊆ On × On
31 22 fndmi ⊢ dom ⁡ + = On × On
32 30 31 sseqtrrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A × B + C ⊆ dom ⁡ +
33 funimassov ⊢ Fun ⁡ + ∧ A × B + C ⊆ dom ⁡ + → + A × B + C ⊆ x ↔ ∀ a ∈ A ∀ p ∈ B + C a + p ∈ x
34 24 32 33 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × B + C ⊆ x ↔ ∀ a ∈ A ∀ p ∈ B + C a + p ∈ x
35 ovex ⊢ B + C ∈ V
36 oveq2 ⊢ p = B + C → a + p = a + B + C
37 36 eleq1d ⊢ p = B + C → a + p ∈ x ↔ a + B + C ∈ x
38 35 37 ralsn ⊢ ∀ p ∈ B + C a + p ∈ x ↔ a + B + C ∈ x
39 38 ralbii ⊢ ∀ a ∈ A ∀ p ∈ B + C a + p ∈ x ↔ ∀ a ∈ A a + B + C ∈ x
40 34 39 bitrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × B + C ⊆ x ↔ ∀ a ∈ A a + B + C ∈ x
41 simpl1 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A ∈ On
42 41 snssd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A ⊆ On
43 imassrn ⊢ + B × C ⊆ ran ⁡ +
44 naddf ⊢ + : On × On ⟶ On
45 frn ⊢ + : On × On ⟶ On → ran ⁡ + ⊆ On
46 44 45 ax-mp ⊢ ran ⁡ + ⊆ On
47 43 46 sstri ⊢ + B × C ⊆ On
48 xpss12 ⊢ A ⊆ On ∧ + B × C ⊆ On → A × + B × C ⊆ On × On
49 42 47 48 sylancl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A × + B × C ⊆ On × On
50 49 31 sseqtrrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A × + B × C ⊆ dom ⁡ +
51 funimassov ⊢ Fun ⁡ + ∧ A × + B × C ⊆ dom ⁡ + → + A × + B × C ⊆ x ↔ ∀ a ∈ A ∀ p ∈ + B × C a + p ∈ x
52 24 50 51 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × + B × C ⊆ x ↔ ∀ a ∈ A ∀ p ∈ + B × C a + p ∈ x
53 oveq1 ⊢ a = A → a + p = A + p
54 53 eleq1d ⊢ a = A → a + p ∈ x ↔ A + p ∈ x
55 54 ralbidv ⊢ a = A → ∀ p ∈ + B × C a + p ∈ x ↔ ∀ p ∈ + B × C A + p ∈ x
56 55 ralsng ⊢ A ∈ On → ∀ a ∈ A ∀ p ∈ + B × C a + p ∈ x ↔ ∀ p ∈ + B × C A + p ∈ x
57 41 56 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ a ∈ A ∀ p ∈ + B × C a + p ∈ x ↔ ∀ p ∈ + B × C A + p ∈ x
58 onss ⊢ B ∈ On → B ⊆ On
59 58 3ad2ant2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → B ⊆ On
60 simpl3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → C ∈ On
61 60 snssd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → C ⊆ On
62 xpss12 ⊢ B ⊆ On ∧ C ⊆ On → B × C ⊆ On × On
63 59 61 62 syl2an2r ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B × C ⊆ On × On
64 oveq2 ⊢ p = b + c → A + p = A + b + c
65 64 eleq1d ⊢ p = b + c → A + p ∈ x ↔ A + b + c ∈ x
66 65 imaeqalov ⊢ + Fn On × On ∧ B × C ⊆ On × On → ∀ p ∈ + B × C A + p ∈ x ↔ ∀ b ∈ B ∀ c ∈ C A + b + c ∈ x
67 22 63 66 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + B × C A + p ∈ x ↔ ∀ b ∈ B ∀ c ∈ C A + b + c ∈ x
68 oveq2 ⊢ c = C → b + c = b + C
69 68 oveq2d ⊢ c = C → A + b + c = A + b + C
70 69 eleq1d ⊢ c = C → A + b + c ∈ x ↔ A + b + C ∈ x
71 70 ralsng ⊢ C ∈ On → ∀ c ∈ C A + b + c ∈ x ↔ A + b + C ∈ x
72 60 71 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ c ∈ C A + b + c ∈ x ↔ A + b + C ∈ x
73 72 ralbidv ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ b ∈ B ∀ c ∈ C A + b + c ∈ x ↔ ∀ b ∈ B A + b + C ∈ x
74 67 73 bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + B × C A + p ∈ x ↔ ∀ b ∈ B A + b + C ∈ x
75 52 57 74 3bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × + B × C ⊆ x ↔ ∀ b ∈ B A + b + C ∈ x
76 imassrn ⊢ + B × C ⊆ ran ⁡ +
77 76 46 sstri ⊢ + B × C ⊆ On
78 xpss12 ⊢ A ⊆ On ∧ + B × C ⊆ On → A × + B × C ⊆ On × On
79 42 77 78 sylancl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A × + B × C ⊆ On × On
80 79 31 sseqtrrdi ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → A × + B × C ⊆ dom ⁡ +
81 funimassov ⊢ Fun ⁡ + ∧ A × + B × C ⊆ dom ⁡ + → + A × + B × C ⊆ x ↔ ∀ a ∈ A ∀ p ∈ + B × C a + p ∈ x
82 24 80 81 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × + B × C ⊆ x ↔ ∀ a ∈ A ∀ p ∈ + B × C a + p ∈ x
83 54 ralbidv ⊢ a = A → ∀ p ∈ + B × C a + p ∈ x ↔ ∀ p ∈ + B × C A + p ∈ x
84 83 ralsng ⊢ A ∈ On → ∀ a ∈ A ∀ p ∈ + B × C a + p ∈ x ↔ ∀ p ∈ + B × C A + p ∈ x
85 41 84 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ a ∈ A ∀ p ∈ + B × C a + p ∈ x ↔ ∀ p ∈ + B × C A + p ∈ x
86 simpl2 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B ∈ On
87 86 snssd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B ⊆ On
88 onss ⊢ C ∈ On → C ⊆ On
89 88 3ad2ant3 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → C ⊆ On
90 89 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → C ⊆ On
91 xpss12 ⊢ B ⊆ On ∧ C ⊆ On → B × C ⊆ On × On
92 87 90 91 syl2anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → B × C ⊆ On × On
93 65 imaeqalov ⊢ + Fn On × On ∧ B × C ⊆ On × On → ∀ p ∈ + B × C A + p ∈ x ↔ ∀ b ∈ B ∀ c ∈ C A + b + c ∈ x
94 22 92 93 sylancr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + B × C A + p ∈ x ↔ ∀ b ∈ B ∀ c ∈ C A + b + c ∈ x
95 oveq1 ⊢ b = B → b + c = B + c
96 95 oveq2d ⊢ b = B → A + b + c = A + B + c
97 96 eleq1d ⊢ b = B → A + b + c ∈ x ↔ A + B + c ∈ x
98 97 ralbidv ⊢ b = B → ∀ c ∈ C A + b + c ∈ x ↔ ∀ c ∈ C A + B + c ∈ x
99 98 ralsng ⊢ B ∈ On → ∀ b ∈ B ∀ c ∈ C A + b + c ∈ x ↔ ∀ c ∈ C A + B + c ∈ x
100 86 99 syl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ b ∈ B ∀ c ∈ C A + b + c ∈ x ↔ ∀ c ∈ C A + B + c ∈ x
101 94 100 bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → ∀ p ∈ + B × C A + p ∈ x ↔ ∀ c ∈ C A + B + c ∈ x
102 82 85 101 3bitrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ x ∈ On → + A × + B × C ⊆ x ↔ ∀ c ∈ C A + B + c ∈ x
103 40 75 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 + C ∪ + A × + B × C ∪ + 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 + C ∪ + A × + B × C ∪ + 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 + C ∪ + A × + B × C ∪ + 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