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