Theorem onssmin

Description: A nonempty class of ordinal numbers has the smallest member. Exercise 9 of TakeutiZaring p. 40. (Contributed by NM, 3-Oct-2003)

	Ref	Expression
Assertion	onssmin	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		onint	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )
2		intss1	⊢ ( 𝑦 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑦 )
3	2	rgen	⊢ ∀ 𝑦 ∈ 𝐴 ∩ 𝐴 ⊆ 𝑦
4		sseq1	⊢ ( 𝑥 = ∩ 𝐴 → ( 𝑥 ⊆ 𝑦 ↔ ∩ 𝐴 ⊆ 𝑦 ) )
5	4	ralbidv	⊢ ( 𝑥 = ∩ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ∩ 𝐴 ⊆ 𝑦 ) )
6	5	rspcev	⊢ ( ( ∩ 𝐴 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ∩ 𝐴 ⊆ 𝑦 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
7	1 3 6	sylancl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )