Metamath Proof Explorer

Theorem naddrid

Description: Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion naddrid ⊢ A ∈ On → A + ∅ = A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ a = b → a + ∅ = b + ∅
2 id ⊢ a = b → a = b
3 1 2 eqeq12d ⊢ a = b → a + ∅ = a ↔ b + ∅ = b
4 oveq1 ⊢ a = A → a + ∅ = A + ∅
5 id ⊢ a = A → a = A
6 4 5 eqeq12d ⊢ a = A → a + ∅ = a ↔ A + ∅ = A
7 0elon ⊢ ∅ ∈ On
8 naddov2 ⊢ a ∈ On ∧ ∅ ∈ On → a + ∅ = ⋂ x ∈ On | ∀ c ∈ ∅ a + c ∈ x ∧ ∀ b ∈ a b + ∅ ∈ x
9 7 8 mpan2 ⊢ a ∈ On → a + ∅ = ⋂ x ∈ On | ∀ c ∈ ∅ a + c ∈ x ∧ ∀ b ∈ a b + ∅ ∈ x
10 9 adantr ⊢ a ∈ On ∧ ∀ b ∈ a b + ∅ = b → a + ∅ = ⋂ x ∈ On | ∀ c ∈ ∅ a + c ∈ x ∧ ∀ b ∈ a b + ∅ ∈ x
11 ral0 ⊢ ∀ c ∈ ∅ a + c ∈ x
12 11 biantrur ⊢ ∀ b ∈ a b + ∅ ∈ x ↔ ∀ c ∈ ∅ a + c ∈ x ∧ ∀ b ∈ a b + ∅ ∈ x
13 eleq1 ⊢ b + ∅ = b → b + ∅ ∈ x ↔ b ∈ x
14 13 ralimi ⊢ ∀ b ∈ a b + ∅ = b → ∀ b ∈ a b + ∅ ∈ x ↔ b ∈ x
15 ralbi ⊢ ∀ b ∈ a b + ∅ ∈ x ↔ b ∈ x → ∀ b ∈ a b + ∅ ∈ x ↔ ∀ b ∈ a b ∈ x
16 14 15 syl ⊢ ∀ b ∈ a b + ∅ = b → ∀ b ∈ a b + ∅ ∈ x ↔ ∀ b ∈ a b ∈ x
17 16 adantl ⊢ a ∈ On ∧ ∀ b ∈ a b + ∅ = b → ∀ b ∈ a b + ∅ ∈ x ↔ ∀ b ∈ a b ∈ x
18 dfss3 ⊢ a ⊆ x ↔ ∀ b ∈ a b ∈ x
19 17 18 bitr4di ⊢ a ∈ On ∧ ∀ b ∈ a b + ∅ = b → ∀ b ∈ a b + ∅ ∈ x ↔ a ⊆ x
20 12 19 bitr3id ⊢ a ∈ On ∧ ∀ b ∈ a b + ∅ = b → ∀ c ∈ ∅ a + c ∈ x ∧ ∀ b ∈ a b + ∅ ∈ x ↔ a ⊆ x
21 20 rabbidv ⊢ a ∈ On ∧ ∀ b ∈ a b + ∅ = b → x ∈ On | ∀ c ∈ ∅ a + c ∈ x ∧ ∀ b ∈ a b + ∅ ∈ x = x ∈ On | a ⊆ x
22 21 inteqd ⊢ a ∈ On ∧ ∀ b ∈ a b + ∅ = b → ⋂ x ∈ On | ∀ c ∈ ∅ a + c ∈ x ∧ ∀ b ∈ a b + ∅ ∈ x = ⋂ x ∈ On | a ⊆ x
23 intmin ⊢ a ∈ On → ⋂ x ∈ On | a ⊆ x = a
24 23 adantr ⊢ a ∈ On ∧ ∀ b ∈ a b + ∅ = b → ⋂ x ∈ On | a ⊆ x = a
25 10 22 24 3eqtrd ⊢ a ∈ On ∧ ∀ b ∈ a b + ∅ = b → a + ∅ = a
26 25 ex ⊢ a ∈ On → ∀ b ∈ a b + ∅ = b → a + ∅ = a
27 3 6 26 tfis3 ⊢ A ∈ On → A + ∅ = A