Theorem scottn0f

Description: A version of scott0f with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018)

	Ref	Expression
Hypotheses	scottn0f.1	⊢ Ⅎ 𝑦 𝐴
	scottn0f.2	⊢ Ⅎ 𝑥 𝐴
Assertion	scottn0f	⊢ ( 𝐴 ≠ ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		scottn0f.1	⊢ Ⅎ 𝑦 𝐴
2		scottn0f.2	⊢ Ⅎ 𝑥 𝐴
3	1 2	scott0f	⊢ ( 𝐴 = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )
4	3	necon3bii	⊢ ( 𝐴 ≠ ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ )