Metamath Proof Explorer


Theorem scotteld

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

Ref Expression
Hypothesis scotteld.1 φ x x A
Assertion scotteld φ x x Scott A

Proof

Step Hyp Ref Expression
1 scotteld.1 φ x x A
2 n0 A x x A
3 1 2 sylibr φ A
4 3 neneqd φ ¬ A =
5 scott0 A = y A | z A rank y rank z =
6 df-scott Scott A = y A | z A rank y rank z
7 6 eqeq1i Scott A = y A | z A rank y rank z =
8 5 7 bitr4i A = Scott A =
9 4 8 sylnib φ ¬ Scott A =
10 9 neqned φ Scott A
11 n0 Scott A x x Scott A
12 10 11 sylib φ x x Scott A