Theorem onintss

Description: If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of Suppes p. 228. (Contributed by NM, 3-Oct-2003)

	Ref	Expression
Hypothesis	onintss.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	onintss	⊢ ( 𝐴 ∈ On → ( 𝜓 → ∩ { 𝑥 ∈ On ∣ 𝜑 } ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		onintss.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2	1	intminss	⊢ ( ( 𝐴 ∈ On ∧ 𝜓 ) → ∩ { 𝑥 ∈ On ∣ 𝜑 } ⊆ 𝐴 )
3	2	ex	⊢ ( 𝐴 ∈ On → ( 𝜓 → ∩ { 𝑥 ∈ On ∣ 𝜑 } ⊆ 𝐴 ) )