Theorem sadid1

Description: The adder sequence function has a left identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Assertion	sadid1	⊢ ( 𝐴 ⊆ ℕ0 → ( 𝐴 sadd ∅ ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ⊆ ℕ0 → 𝐴 ⊆ ℕ0 )
2		0ss	⊢ ∅ ⊆ ℕ0
3	2	a1i	⊢ ( 𝐴 ⊆ ℕ0 → ∅ ⊆ ℕ0 )
4		in0	⊢ ( 𝐴 ∩ ∅ ) = ∅
5	4	a1i	⊢ ( 𝐴 ⊆ ℕ0 → ( 𝐴 ∩ ∅ ) = ∅ )
6	1 3 5	saddisj	⊢ ( 𝐴 ⊆ ℕ0 → ( 𝐴 sadd ∅ ) = ( 𝐴 ∪ ∅ ) )
7		un0	⊢ ( 𝐴 ∪ ∅ ) = 𝐴
8	6 7	eqtrdi	⊢ ( 𝐴 ⊆ ℕ0 → ( 𝐴 sadd ∅ ) = 𝐴 )