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 ⊢ Ⅎ x ψ
onminsb.2 ⊢ x = ⋂ x ∈ On | φ → φ ↔ ψ
Assertion onminsb ⊢ ∃ x ∈ On φ → ψ

Proof

Step Hyp Ref Expression
1 onminsb.1 ⊢ Ⅎ x ψ
2 onminsb.2 ⊢ x = ⋂ x ∈ On | φ → φ ↔ ψ
3 rabn0 ⊢ x ∈ On | φ ≠ ∅ ↔ ∃ x ∈ On φ
4 ssrab2 ⊢ x ∈ On | φ ⊆ On
5 onint ⊢ x ∈ On | φ ⊆ On ∧ x ∈ On | φ ≠ ∅ → ⋂ x ∈ On | φ ∈ x ∈ On | φ
6 4 5 mpan ⊢ x ∈ On | φ ≠ ∅ → ⋂ x ∈ On | φ ∈ x ∈ On | φ
7 3 6 sylbir ⊢ ∃ x ∈ On φ → ⋂ x ∈ On | φ ∈ x ∈ On | φ
8 nfrab1 ⊢ Ⅎ _ x x ∈ On | φ
9 8 nfint ⊢ Ⅎ _ x ⋂ x ∈ On | φ
10 nfcv ⊢ Ⅎ _ x On
11 9 10 1 2 elrabf ⊢ ⋂ x ∈ On | φ ∈ x ∈ On | φ ↔ ⋂ x ∈ On | φ ∈ On ∧ ψ
12 11 simprbi ⊢ ⋂ x ∈ On | φ ∈ x ∈ On | φ → ψ
13 7 12 syl ⊢ ∃ x ∈ On φ → ψ