Theorem scottex

Description: Scott's trick produces a set. (Contributed by NM, 13-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 18-Jul-2026)

	Ref	Expression
Assertion	scottex	⊢ Scott 𝐴 ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-scott	⊢ Scott 𝐴 = { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
2		0ex	⊢ ∅ ∈ V
3		eleq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ V ↔ ∅ ∈ V ) )
4	2 3	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ∈ V )
5		rabexg	⊢ ( 𝐴 ∈ V → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
6	4 5	syl	⊢ ( 𝐴 = ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
7		neq0	⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑣 𝑣 ∈ 𝐴 )
8		fveq2	⊢ ( 𝑦 = 𝑣 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝑣 ) )
9	8	sseq2d	⊢ ( 𝑦 = 𝑣 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) ) )
10	9	rspcv	⊢ ( 𝑣 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) ) )
11	10	adantr	⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) ) )
12	11	ss2rabdv	⊢ ( 𝑣 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } )
13		rankon	⊢ ( rank ‘ 𝑣 ) ∈ On
14		fveq2	⊢ ( 𝑥 = 𝑤 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑤 ) )
15	14	sseq1d	⊢ ( 𝑥 = 𝑤 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) ↔ ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑣 ) ) )
16	15	elrab	⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ↔ ( 𝑤 ∈ 𝐴 ∧ ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑣 ) ) )
17	16	simprbi	⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } → ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑣 ) )
18	17	rgen	⊢ ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑣 )
19		sseq2	⊢ ( 𝑧 = ( rank ‘ 𝑣 ) → ( ( rank ‘ 𝑤 ) ⊆ 𝑧 ↔ ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑣 ) ) )
20	19	ralbidv	⊢ ( 𝑧 = ( rank ‘ 𝑣 ) → ( ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ( rank ‘ 𝑤 ) ⊆ 𝑧 ↔ ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑣 ) ) )
21	20	rspcev	⊢ ( ( ( rank ‘ 𝑣 ) ∈ On ∧ ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑣 ) ) → ∃ 𝑧 ∈ On ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ( rank ‘ 𝑤 ) ⊆ 𝑧 )
22	13 18 21	mp2an	⊢ ∃ 𝑧 ∈ On ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ( rank ‘ 𝑤 ) ⊆ 𝑧
23		bndrank	⊢ ( ∃ 𝑧 ∈ On ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ( rank ‘ 𝑤 ) ⊆ 𝑧 → { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ∈ V )
24	22 23	ax-mp	⊢ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } ∈ V
25	24	ssex	⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑣 ) } → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
26	12 25	syl	⊢ ( 𝑣 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
27	26	exlimiv	⊢ ( ∃ 𝑣 𝑣 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
28	7 27	sylbi	⊢ ( ¬ 𝐴 = ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
29	6 28	pm2.61i	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V
30	1 29	eqeltri	⊢ Scott 𝐴 ∈ V