Theorem onminesb

Description: If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of Suppes p. 228. (Contributed by NM, 29-Sep-2003)

	Ref	Expression
Assertion	onminesb	⊢ ( ∃ 𝑥 ∈ On 𝜑 → [ ∩ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rabn0	⊢ ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝜑 )
2		ssrab2	⊢ { 𝑥 ∈ On ∣ 𝜑 } ⊆ On
3		onint	⊢ ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ) → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } )
4	2 3	mpan	⊢ ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } )
5	1 4	sylbir	⊢ ( ∃ 𝑥 ∈ On 𝜑 → ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } )
6		nfcv	⊢ Ⅎ 𝑥 On
7	6	elrabsf	⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On ∧ [ ∩ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 ) )
8	7	simprbi	⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } → [ ∩ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 )
9	5 8	syl	⊢ ( ∃ 𝑥 ∈ On 𝜑 → [ ∩ { 𝑥 ∈ On ∣ 𝜑 } / 𝑥 ] 𝜑 )