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	|- F/_ y A
	scott0f.2	|- F/_ x A
Assertion	scott0f	|- ( A = (/) <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) )

Proof

Step	Hyp	Ref	Expression
1		scott0f.1	|- F/_ y A
2		scott0f.2	|- F/_ x A
3		df-scott	|- Scott A = { w e. A | A. z e. A ( rank ` w ) C_ ( rank ` z ) }
4	3	eqeq1i	|- ( Scott A = (/) <-> { w e. A | A. z e. A ( rank ` w ) C_ ( rank ` z ) } = (/) )
5		scott0b	|- ( A = (/) <-> Scott A = (/) )
6		nfcv	|- F/_ z A
7		nfv	|- F/ z ( rank ` x ) C_ ( rank ` y )
8		nfv	|- F/ y ( rank ` x ) C_ ( rank ` z )
9		fveq2	|- ( y = z -> ( rank ` y ) = ( rank ` z ) )
10	9	sseq2d	|- ( y = z -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` x ) C_ ( rank ` z ) ) )
11	1 6 7 8 10	cbvralfw	|- ( A. y e. A ( rank ` x ) C_ ( rank ` y ) <-> A. z e. A ( rank ` x ) C_ ( rank ` z ) )
12	11	rabbii	|- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = { x e. A | A. z e. A ( rank ` x ) C_ ( rank ` z ) }
13		nfcv	|- F/_ w A
14		nfv	|- F/ x ( rank ` w ) C_ ( rank ` z )
15	2 14	nfralw	|- F/ x A. z e. A ( rank ` w ) C_ ( rank ` z )
16		nfv	|- F/ w A. z e. A ( rank ` x ) C_ ( rank ` z )
17		fveq2	|- ( w = x -> ( rank ` w ) = ( rank ` x ) )
18	17	sseq1d	|- ( w = x -> ( ( rank ` w ) C_ ( rank ` z ) <-> ( rank ` x ) C_ ( rank ` z ) ) )
19	18	ralbidv	|- ( w = x -> ( A. z e. A ( rank ` w ) C_ ( rank ` z ) <-> A. z e. A ( rank ` x ) C_ ( rank ` z ) ) )
20	13 2 15 16 19	cbvrabw	|- { w e. A | A. z e. A ( rank ` w ) C_ ( rank ` z ) } = { x e. A | A. z e. A ( rank ` x ) C_ ( rank ` z ) }
21	12 20	eqtr4i	|- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = { w e. A | A. z e. A ( rank ` w ) C_ ( rank ` z ) }
22	21	eqeq1i	|- ( { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) <-> { w e. A | A. z e. A ( rank ` w ) C_ ( rank ` z ) } = (/) )
23	4 5 22	3bitr4i	|- ( A = (/) <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) )