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		scott0	⊢ ( 𝐴 = ∅ ↔ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) } = ∅ )
6		df-scott	⊢ Scott 𝐴 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) }
7	6	eqeq1i	⊢ ( Scott 𝐴 = ∅ ↔ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑧 ∈ 𝐴 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) } = ∅ )
8	5 7	bitr4i	⊢ ( 𝐴 = ∅ ↔ Scott 𝐴 = ∅ )
9	4 8	sylnib	⊢ ( 𝜑 → ¬ Scott 𝐴 = ∅ )
10	9	neqned	⊢ ( 𝜑 → Scott 𝐴 ≠ ∅ )
11		n0	⊢ ( Scott 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ Scott 𝐴 )
12	10 11	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ Scott 𝐴 )