Metamath Proof Explorer


Theorem onminsb

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

Ref Expression
Hypotheses onminsb.1 𝑥 𝜓
onminsb.2 ( 𝑥 = { 𝑥 ∈ On ∣ 𝜑 } → ( 𝜑𝜓 ) )
Assertion onminsb ( ∃ 𝑥 ∈ On 𝜑𝜓 )

Proof

Step Hyp Ref Expression
1 onminsb.1 𝑥 𝜓
2 onminsb.2 ( 𝑥 = { 𝑥 ∈ On ∣ 𝜑 } → ( 𝜑𝜓 ) )
3 rabn0 ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝜑 )
4 ssrab2 { 𝑥 ∈ On ∣ 𝜑 } ⊆ On
5 onint ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ ) → { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } )
6 4 5 mpan ( { 𝑥 ∈ On ∣ 𝜑 } ≠ ∅ → { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } )
7 3 6 sylbir ( ∃ 𝑥 ∈ On 𝜑 { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } )
8 nfrab1 𝑥 { 𝑥 ∈ On ∣ 𝜑 }
9 8 nfint 𝑥 { 𝑥 ∈ On ∣ 𝜑 }
10 nfcv 𝑥 On
11 9 10 1 2 elrabf ( { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( { 𝑥 ∈ On ∣ 𝜑 } ∈ On ∧ 𝜓 ) )
12 11 simprbi ( { 𝑥 ∈ On ∣ 𝜑 } ∈ { 𝑥 ∈ On ∣ 𝜑 } → 𝜓 )
13 7 12 syl ( ∃ 𝑥 ∈ On 𝜑𝜓 )