Metamath Proof Explorer

Theorem un0addcl

Description: If S is closed under addition, then so is S u. { 0 } . (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Hypotheses un0addcl.1 ⊢ φ → S ⊆ ℂ
un0addcl.2 ⊢ T = S ∪ 0
un0addcl.3 ⊢ φ ∧ M ∈ S ∧ N ∈ S → M + N ∈ S
Assertion un0addcl ⊢ φ ∧ M ∈ T ∧ N ∈ T → M + N ∈ T

Proof

Step Hyp Ref Expression
1 un0addcl.1 ⊢ φ → S ⊆ ℂ
2 un0addcl.2 ⊢ T = S ∪ 0
3 un0addcl.3 ⊢ φ ∧ M ∈ S ∧ N ∈ S → M + N ∈ S
4 2 eleq2i ⊢ N ∈ T ↔ N ∈ S ∪ 0
5 elun ⊢ N ∈ S ∪ 0 ↔ N ∈ S ∨ N ∈ 0
6 4 5 bitri ⊢ N ∈ T ↔ N ∈ S ∨ N ∈ 0
7 2 eleq2i ⊢ M ∈ T ↔ M ∈ S ∪ 0
8 elun ⊢ M ∈ S ∪ 0 ↔ M ∈ S ∨ M ∈ 0
9 7 8 bitri ⊢ M ∈ T ↔ M ∈ S ∨ M ∈ 0
10 ssun1 ⊢ S ⊆ S ∪ 0
11 10 2 sseqtrri ⊢ S ⊆ T
12 11 3 sselid ⊢ φ ∧ M ∈ S ∧ N ∈ S → M + N ∈ T
13 12 expr ⊢ φ ∧ M ∈ S → N ∈ S → M + N ∈ T
14 1 sselda ⊢ φ ∧ N ∈ S → N ∈ ℂ
15 14 addlidd ⊢ φ ∧ N ∈ S → 0 + N = N
16 11 a1i ⊢ φ → S ⊆ T
17 16 sselda ⊢ φ ∧ N ∈ S → N ∈ T
18 15 17 eqeltrd ⊢ φ ∧ N ∈ S → 0 + N ∈ T
19 elsni ⊢ M ∈ 0 → M = 0
20 19 oveq1d ⊢ M ∈ 0 → M + N = 0 + N
21 20 eleq1d ⊢ M ∈ 0 → M + N ∈ T ↔ 0 + N ∈ T
22 18 21 syl5ibrcom ⊢ φ ∧ N ∈ S → M ∈ 0 → M + N ∈ T
23 22 impancom ⊢ φ ∧ M ∈ 0 → N ∈ S → M + N ∈ T
24 13 23 jaodan ⊢ φ ∧ M ∈ S ∨ M ∈ 0 → N ∈ S → M + N ∈ T
25 9 24 sylan2b ⊢ φ ∧ M ∈ T → N ∈ S → M + N ∈ T
26 0cnd ⊢ φ → 0 ∈ ℂ
27 26 snssd ⊢ φ → 0 ⊆ ℂ
28 1 27 unssd ⊢ φ → S ∪ 0 ⊆ ℂ
29 2 28 eqsstrid ⊢ φ → T ⊆ ℂ
30 29 sselda ⊢ φ ∧ M ∈ T → M ∈ ℂ
31 30 addridd ⊢ φ ∧ M ∈ T → M + 0 = M
32 simpr ⊢ φ ∧ M ∈ T → M ∈ T
33 31 32 eqeltrd ⊢ φ ∧ M ∈ T → M + 0 ∈ T
34 elsni ⊢ N ∈ 0 → N = 0
35 34 oveq2d ⊢ N ∈ 0 → M + N = M + 0
36 35 eleq1d ⊢ N ∈ 0 → M + N ∈ T ↔ M + 0 ∈ T
37 33 36 syl5ibrcom ⊢ φ ∧ M ∈ T → N ∈ 0 → M + N ∈ T
38 25 37 jaod ⊢ φ ∧ M ∈ T → N ∈ S ∨ N ∈ 0 → M + N ∈ T
39 6 38 biimtrid ⊢ φ ∧ M ∈ T → N ∈ T → M + N ∈ T
40 39 impr ⊢ φ ∧ M ∈ T ∧ N ∈ T → M + N ∈ T