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	⊢ ( ∅ ∈ 𝐴 → Scott 𝐴 = { ∅ } )

Proof

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