Theorem onsucmin

Description: The successor of an ordinal number is the smallest larger ordinal number. (Contributed by NM, 28-Nov-2003)

	Ref	Expression
Assertion	onsucmin	⊢ ( 𝐴 ∈ On → suc 𝐴 = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝑥 ∈ On → Ord 𝑥 )
2		ordelsuc	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝑥 ) → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 ∈ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) )
4	3	rabbidva	⊢ ( 𝐴 ∈ On → { 𝑥 ∈ On ∣ 𝐴 ∈ 𝑥 } = { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } )
5	4	inteqd	⊢ ( 𝐴 ∈ On → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ 𝑥 } = ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } )
6		sucelon	⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )
7		intmin	⊢ ( suc 𝐴 ∈ On → ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } = suc 𝐴 )
8	6 7	sylbi	⊢ ( 𝐴 ∈ On → ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } = suc 𝐴 )
9	5 8	eqtr2d	⊢ ( 𝐴 ∈ On → suc 𝐴 = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ 𝑥 } )