Theorem scott0f

Description: A version of scott0b with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018)

	Ref	Expression
Hypotheses	scott0f.1	⊢ Ⅎ 𝑦 𝐴
	scott0f.2	⊢ Ⅎ 𝑥 𝐴
Assertion	scott0f	⊢ ( 𝐴 = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		scott0f.1	⊢ Ⅎ 𝑦 𝐴
2		scott0f.2	⊢ Ⅎ 𝑥 𝐴
3		df-scott	⊢ Scott 𝐴 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) }
4	3	eqeq1i	⊢ ( Scott 𝐴 = ∅ ↔ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) } = ∅ )
5		scott0b	⊢ ( 𝐴 = ∅ ↔ Scott 𝐴 = ∅ )
6		nfcv	⊢ Ⅎ 𝑧 𝐴
7		nfv	⊢ Ⅎ 𝑧 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 )
8		nfv	⊢ Ⅎ 𝑦 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 )
9		fveq2	⊢ ( 𝑦 = 𝑧 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) )
10	9	sseq2d	⊢ ( 𝑦 = 𝑧 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) ) )
11	1 6 7 8 10	cbvralfw	⊢ ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) )
12	11	rabbii	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) }
13		nfcv	⊢ Ⅎ 𝑤 𝐴
14		nfv	⊢ Ⅎ 𝑥 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 )
15	2 14	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 )
16		nfv	⊢ Ⅎ 𝑤 ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 )
17		fveq2	⊢ ( 𝑤 = 𝑥 → ( rank ‘ 𝑤 ) = ( rank ‘ 𝑥 ) )
18	17	sseq1d	⊢ ( 𝑤 = 𝑥 → ( ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) ) )
19	18	ralbidv	⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) ) )
20	13 2 15 16 19	cbvrabw	⊢ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) } = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑧 ) }
21	12 20	eqtr4i	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) }
22	21	eqeq1i	⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ ↔ { 𝑤 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑧 ) } = ∅ )
23	4 5 22	3bitr4i	⊢ ( 𝐴 = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )