Metamath Proof Explorer

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 A ∈ V

Proof

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