Theorem scotteld

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

	Ref	Expression
Hypothesis	scotteld.1	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 )
Assertion	scotteld	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ Scott 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		scotteld.1	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 )
2		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
3	1 2	sylibr	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
4	3	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = ∅ )
5		scott0b	⊢ ( 𝐴 = ∅ ↔ Scott 𝐴 = ∅ )
6	4 5	sylnib	⊢ ( 𝜑 → ¬ Scott 𝐴 = ∅ )
7	6	neqned	⊢ ( 𝜑 → Scott 𝐴 ≠ ∅ )
8		n0	⊢ ( Scott 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ Scott 𝐴 )
9	7 8	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ Scott 𝐴 )