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		scott0b	|- ( A = (/) <-> Scott A = (/) )
6	4 5	sylnib	|- ( ph -> -. Scott A = (/) )
7	6	neqned	|- ( ph -> Scott A =/= (/) )
8		n0	|- ( Scott A =/= (/) <-> E. x x e. Scott A )
9	7 8	sylib	|- ( ph -> E. x x e. Scott A )