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

Metamath Proof Explorer

Theorem scottexs

Description: Theorem scheme version of scottex . The collection of all x of minimum rank such that ph ( x ) is true, is a set. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion scottexs { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ∈ V

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ 𝑧 { 𝑥 ∣ 𝜑 }
2 nfab1 ⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
3 nfv ⊢ Ⅎ 𝑥 ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 )
4 2 3 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 )
5 nfv ⊢ Ⅎ 𝑧 ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 )
6 fveq2 ⊢ ( 𝑧 = 𝑥 → ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) )
7 6 sseq1d ⊢ ( 𝑧 = 𝑥 → ( ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
8 7 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
9 1 2 4 5 8 cbvrabw ⊢ { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
10 df-rab ⊢ { 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∣ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) }
11 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
12 df-ral ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
13 df-sbc ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
14 13 imbi1i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
15 14 albii ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
16 12 15 bitr4i ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
17 11 16 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
18 17 abbii ⊢ { 𝑥 ∣ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
19 9 10 18 3eqtri ⊢ { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
20 scottex ⊢ { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V
21 19 20 eqeltrri ⊢ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ∈ V