This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V

Proof

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