Theorem naddid1

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

	Ref	Expression
Assertion	naddid1	⊢ ( 𝐴 ∈ On → ( 𝐴 +no ∅ ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 +no ∅ ) = ( 𝑏 +no ∅ ) )
2		id	⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 )
3	1 2	eqeq12d	⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 +no ∅ ) = 𝑎 ↔ ( 𝑏 +no ∅ ) = 𝑏 ) )
4		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 +no ∅ ) = ( 𝐴 +no ∅ ) )
5		id	⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
6	4 5	eqeq12d	⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +no ∅ ) = 𝑎 ↔ ( 𝐴 +no ∅ ) = 𝐴 ) )
7		0elon	⊢ ∅ ∈ On
8		naddov2	⊢ ( ( 𝑎 ∈ On ∧ ∅ ∈ On ) → ( 𝑎 +no ∅ ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ ∅ ( 𝑎 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ) } )
9	7 8	mpan2	⊢ ( 𝑎 ∈ On → ( 𝑎 +no ∅ ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ ∅ ( 𝑎 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ) } )
10	9	adantr	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 ) → ( 𝑎 +no ∅ ) = ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ ∅ ( 𝑎 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ) } )
11		ral0	⊢ ∀ 𝑐 ∈ ∅ ( 𝑎 +no 𝑐 ) ∈ 𝑥
12	11	biantrur	⊢ ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ↔ ( ∀ 𝑐 ∈ ∅ ( 𝑎 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ) )
13		eleq1	⊢ ( ( 𝑏 +no ∅ ) = 𝑏 → ( ( 𝑏 +no ∅ ) ∈ 𝑥 ↔ 𝑏 ∈ 𝑥 ) )
14	13	ralimi	⊢ ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 → ∀ 𝑏 ∈ 𝑎 ( ( 𝑏 +no ∅ ) ∈ 𝑥 ↔ 𝑏 ∈ 𝑥 ) )
15		ralbi	⊢ ( ∀ 𝑏 ∈ 𝑎 ( ( 𝑏 +no ∅ ) ∈ 𝑥 ↔ 𝑏 ∈ 𝑥 ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ 𝑥 ) )
16	14 15	syl	⊢ ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ 𝑥 ) )
17	16	adantl	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ 𝑥 ) )
18		dfss3	⊢ ( 𝑎 ⊆ 𝑥 ↔ ∀ 𝑏 ∈ 𝑎 𝑏 ∈ 𝑥 )
19	17 18	bitr4di	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 ) → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ↔ 𝑎 ⊆ 𝑥 ) )
20	12 19	bitr3id	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 ) → ( ( ∀ 𝑐 ∈ ∅ ( 𝑎 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ) ↔ 𝑎 ⊆ 𝑥 ) )
21	20	rabbidv	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 ) → { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ ∅ ( 𝑎 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ) } = { 𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥 } )
22	21	inteqd	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 ) → ∩ { 𝑥 ∈ On ∣ ( ∀ 𝑐 ∈ ∅ ( 𝑎 +no 𝑐 ) ∈ 𝑥 ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) ∈ 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥 } )
23		intmin	⊢ ( 𝑎 ∈ On → ∩ { 𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥 } = 𝑎 )
24	23	adantr	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 ) → ∩ { 𝑥 ∈ On ∣ 𝑎 ⊆ 𝑥 } = 𝑎 )
25	10 22 24	3eqtrd	⊢ ( ( 𝑎 ∈ On ∧ ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 ) → ( 𝑎 +no ∅ ) = 𝑎 )
26	25	ex	⊢ ( 𝑎 ∈ On → ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 +no ∅ ) = 𝑏 → ( 𝑎 +no ∅ ) = 𝑎 ) )
27	3 6 26	tfis3	⊢ ( 𝐴 ∈ On → ( 𝐴 +no ∅ ) = 𝐴 )