This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 onsucb ⊢ ( 𝐴 ∈ 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 ∣ 𝐴 ∈ 𝑥 } )