Theorem scotteld

Description: The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypothesis	scotteld.1	|- ( ph -> E. x x e. A )
Assertion	scotteld	|- ( ph -> E. x x e. Scott A )

Proof

Step	Hyp	Ref	Expression
1		scotteld.1	|- ( ph -> E. x x e. A )
2		n0	|- ( A =/= (/) <-> E. x x e. A )
3	1 2	sylibr	|- ( ph -> A =/= (/) )
4	3	neneqd	|- ( ph -> -. A = (/) )
5		scott0	|- ( A = (/) <-> { y e. A | A. z e. A ( rank ` y ) C_ ( rank ` z ) } = (/) )
6		df-scott	|- Scott A = { y e. A | A. z e. A ( rank ` y ) C_ ( rank ` z ) }
7	6	eqeq1i	|- ( Scott A = (/) <-> { y e. A | A. z e. A ( rank ` y ) C_ ( rank ` z ) } = (/) )
8	5 7	bitr4i	|- ( A = (/) <-> Scott A = (/) )
9	4 8	sylnib	|- ( ph -> -. Scott A = (/) )
10	9	neqned	|- ( ph -> Scott A =/= (/) )
11		n0	|- ( Scott A =/= (/) <-> E. x x e. Scott A )
12	10 11	sylib	|- ( ph -> E. x x e. Scott A )