Metamath Proof Explorer

Theorem 0elscott

Description: If the empty set is an element of the input class, then the Scott's trick set is the singleton of the empty set. (Contributed by BTernaryTau, 23-Aug-2026)

Ref Expression
Assertion 0elscott ⊢ ∅ ∈ A → Scott A = ∅

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ y = ∅ → rank ⁡ y = rank ⁡ ∅
2 1 sseq2d ⊢ y = ∅ → rank ⁡ x ⊆ rank ⁡ y ↔ rank ⁡ x ⊆ rank ⁡ ∅
3 ss0b ⊢ rank ⁡ x ⊆ ∅ ↔ rank ⁡ x = ∅
4 0elon ⊢ ∅ ∈ On
5 onrankid ⊢ ∅ ∈ On ↔ rank ⁡ ∅ = ∅
6 4 5 mpbi ⊢ rank ⁡ ∅ = ∅
7 6 sseq2i ⊢ rank ⁡ x ⊆ rank ⁡ ∅ ↔ rank ⁡ x ⊆ ∅
8 vex ⊢ x ∈ V
9 8 rankeq0 ⊢ x = ∅ ↔ rank ⁡ x = ∅
10 3 7 9 3bitr4i ⊢ rank ⁡ x ⊆ rank ⁡ ∅ ↔ x = ∅
11 2 10 bitrdi ⊢ y = ∅ → rank ⁡ x ⊆ rank ⁡ y ↔ x = ∅
12 11 rspcv ⊢ ∅ ∈ A → ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y → x = ∅
13 12 ralrimivw ⊢ ∅ ∈ A → ∀ x ∈ A ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y → x = ∅
14 df-scott ⊢ Scott A = x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y
15 14 sseq1i ⊢ Scott A ⊆ ∅ ↔ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ⊆ ∅
16 rabsssn ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ⊆ ∅ ↔ ∀ x ∈ A ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y → x = ∅
17 15 16 bitri ⊢ Scott A ⊆ ∅ ↔ ∀ x ∈ A ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y → x = ∅
18 13 17 sylibr ⊢ ∅ ∈ A → Scott A ⊆ ∅
19 sssn ⊢ Scott A ⊆ ∅ ↔ Scott A = ∅ ∨ Scott A = ∅
20 18 19 sylib ⊢ ∅ ∈ A → Scott A = ∅ ∨ Scott A = ∅
21 elscottn0 ⊢ ∅ ∈ A → Scott A ≠ ∅
22 21 neneqd ⊢ ∅ ∈ A → ¬ Scott A = ∅
23 20 22 orcnd ⊢ ∅ ∈ A → Scott A = ∅