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

Metamath Proof Explorer

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 ∣ 𝜑 } / 𝑥 ] 𝜑 )