Metamath Proof Explorer

Theorem scottex

Description: Scott's trick collects all sets that have a certain property and are of the smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of Jech p. 72, is a set. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion scottex ⊢x∈A|∀y∈Arank⁡x⊆rank⁡y∈V

Proof

Step Hyp Ref Expression
1 0ex ⊢∅∈V
2 eleq1 ⊢A=∅→A∈V↔∅∈V
3 1 2 mpbiri ⊢A=∅→A∈V
4 rabexg ⊢A∈V→x∈A|∀y∈Arank⁡x⊆rank⁡y∈V
5 3 4 syl ⊢A=∅→x∈A|∀y∈Arank⁡x⊆rank⁡y∈V
6 neq0 ⊢¬A=∅↔∃yy∈A
7 nfra1 ⊢Ⅎy∀y∈Arank⁡x⊆rank⁡y
8 nfcv ⊢Ⅎ_yA
9 7 8 nfrabw ⊢Ⅎ_yx∈A|∀y∈Arank⁡x⊆rank⁡y
10 9 nfel1 ⊢Ⅎyx∈A|∀y∈Arank⁡x⊆rank⁡y∈V
11 rsp ⊢∀y∈Arank⁡x⊆rank⁡y→y∈A→rank⁡x⊆rank⁡y
12 11 com12 ⊢y∈A→∀y∈Arank⁡x⊆rank⁡y→rank⁡x⊆rank⁡y
13 12 adantr ⊢y∈A∧x∈A→∀y∈Arank⁡x⊆rank⁡y→rank⁡x⊆rank⁡y
14 13 ss2rabdv ⊢y∈A→x∈A|∀y∈Arank⁡x⊆rank⁡y⊆x∈A|rank⁡x⊆rank⁡y
15 rankon ⊢rank⁡y∈On
16 fveq2 ⊢x=w→rank⁡x=rank⁡w
17 16 sseq1d ⊢x=w→rank⁡x⊆rank⁡y↔rank⁡w⊆rank⁡y
18 17 elrab ⊢w∈x∈A|rank⁡x⊆rank⁡y↔w∈A∧rank⁡w⊆rank⁡y
19 18 simprbi ⊢w∈x∈A|rank⁡x⊆rank⁡y→rank⁡w⊆rank⁡y
20 19 rgen ⊢∀w∈x∈A|rank⁡x⊆rank⁡yrank⁡w⊆rank⁡y
21 sseq2 ⊢z=rank⁡y→rank⁡w⊆z↔rank⁡w⊆rank⁡y
22 21 ralbidv ⊢z=rank⁡y→∀w∈x∈A|rank⁡x⊆rank⁡yrank⁡w⊆z↔∀w∈x∈A|rank⁡x⊆rank⁡yrank⁡w⊆rank⁡y
23 22 rspcev ⊢rank⁡y∈On∧∀w∈x∈A|rank⁡x⊆rank⁡yrank⁡w⊆rank⁡y→∃z∈On∀w∈x∈A|rank⁡x⊆rank⁡yrank⁡w⊆z
24 15 20 23 mp2an ⊢∃z∈On∀w∈x∈A|rank⁡x⊆rank⁡yrank⁡w⊆z
25 bndrank ⊢∃z∈On∀w∈x∈A|rank⁡x⊆rank⁡yrank⁡w⊆z→x∈A|rank⁡x⊆rank⁡y∈V
26 24 25 ax-mp ⊢x∈A|rank⁡x⊆rank⁡y∈V
27 26 ssex ⊢x∈A|∀y∈Arank⁡x⊆rank⁡y⊆x∈A|rank⁡x⊆rank⁡y→x∈A|∀y∈Arank⁡x⊆rank⁡y∈V
28 14 27 syl ⊢y∈A→x∈A|∀y∈Arank⁡x⊆rank⁡y∈V
29 10 28 exlimi ⊢∃yy∈A→x∈A|∀y∈Arank⁡x⊆rank⁡y∈V
30 6 29 sylbi ⊢¬A=∅→x∈A|∀y∈Arank⁡x⊆rank⁡y∈V
31 5 30 pm2.61i ⊢x∈A|∀y∈Arank⁡x⊆rank⁡y∈V