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	ralrimivw	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
14		ss2rab	⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
15	13 14	sylibr	⊢ ( 𝑦 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } )
16		rankon	⊢ ( rank ‘ 𝑦 ) ∈ On
17		fveq2	⊢ ( 𝑥 = 𝑤 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑤 ) )
18	17	sseq1d	⊢ ( 𝑥 = 𝑤 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑦 ) ) )
19	18	elrab	⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ↔ ( 𝑤 ∈ 𝐴 ∧ ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑦 ) ) )
20	19	simprbi	⊢ ( 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } → ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑦 ) )
21	20	rgen	⊢ ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑦 )
22		sseq2	⊢ ( 𝑧 = ( rank ‘ 𝑦 ) → ( ( rank ‘ 𝑤 ) ⊆ 𝑧 ↔ ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑦 ) ) )
23	22	ralbidv	⊢ ( 𝑧 = ( rank ‘ 𝑦 ) → ( ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑤 ) ⊆ 𝑧 ↔ ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑦 ) ) )
24	23	rspcev	⊢ ( ( ( rank ‘ 𝑦 ) ∈ On ∧ ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑤 ) ⊆ ( rank ‘ 𝑦 ) ) → ∃ 𝑧 ∈ On ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑤 ) ⊆ 𝑧 )
25	16 21 24	mp2an	⊢ ∃ 𝑧 ∈ On ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑤 ) ⊆ 𝑧
26		bndrank	⊢ ( ∃ 𝑧 ∈ On ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ( rank ‘ 𝑤 ) ⊆ 𝑧 → { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
27	25 26	ax-mp	⊢ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V
28	27	ssex	⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ⊆ { 𝑥 ∈ 𝐴 ∣ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
29	15 28	syl	⊢ ( 𝑦 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
30	10 29	exlimi	⊢ ( ∃ 𝑦 𝑦 ∈ 𝐴 → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
31	6 30	sylbi	⊢ ( ¬ 𝐴 = ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V )
32	5 31	pm2.61i	⊢ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ∈ V