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