Theorem scott0s

Description: Theorem scheme version of scott0 . The collection of all x of minimum rank such that ph ( x ) is true, is not empty iff there is an x such that ph ( x ) holds. (Contributed by NM, 13-Oct-2003)

	Ref	Expression
Assertion	scott0s	⊢ ( ∃ 𝑥 𝜑 ↔ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ≠ ∅ )

Proof

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