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

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 𝜑 → 𝜓 )