Theorem scott0

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, contains at least one representative with the property, if there is one. In other words, the collection is empty iff no set has the property (i.e. A is empty). (Contributed by NM, 15-Oct-2003)

	Ref	Expression
Assertion	scott0	⊢ ( 𝐴 = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )

Proof

Step	Hyp	Ref	Expression
1		rabeq	⊢ ( 𝐴 = ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∈ ∅ ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } )
2		rab0	⊢ { 𝑥 ∈ ∅ ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅
3	1 2	eqtrdi	⊢ ( 𝐴 = ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )
4		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
5		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 )
6		eqid	⊢ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 )
7		rspe	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
8	6 7	mpan2	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
9	5 8	exlimi	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
10	4 9	sylbi	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
11		fvex	⊢ ( rank ‘ 𝑥 ) ∈ V
12		eqeq1	⊢ ( 𝑦 = ( rank ‘ 𝑥 ) → ( 𝑦 = ( rank ‘ 𝑥 ) ↔ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
13	12	anbi2d	⊢ ( 𝑦 = ( rank ‘ 𝑥 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) ) )
14	11 13	spcev	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) → ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
15	14	eximi	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
16		excom	⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
17	15 16	sylibr	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
18		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
19		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
20	19	exbii	⊢ ( ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
21	17 18 20	3imtr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) )
22	10 21	syl	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) )
23		abn0	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) )
24	22 23	sylibr	⊢ ( 𝐴 ≠ ∅ → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ )
25	11	dfiin2	⊢ ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) }
26		rankon	⊢ ( rank ‘ 𝑥 ) ∈ On
27		eleq1	⊢ ( 𝑦 = ( rank ‘ 𝑥 ) → ( 𝑦 ∈ On ↔ ( rank ‘ 𝑥 ) ∈ On ) )
28	26 27	mpbiri	⊢ ( 𝑦 = ( rank ‘ 𝑥 ) → 𝑦 ∈ On )
29	28	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) → 𝑦 ∈ On )
30	29	abssi	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ⊆ On
31		onint	⊢ ( ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ⊆ On ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } )
32	30 31	mpan	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } )
33	25 32	eqeltrid	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } )
34		nfii1	⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
35	34	nfeq2	⊢ Ⅎ 𝑥 𝑦 = ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
36		eqeq1	⊢ ( 𝑦 = ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) → ( 𝑦 = ( rank ‘ 𝑥 ) ↔ ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
37	35 36	rexbid	⊢ ( 𝑦 = ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
38	37	elabg	⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } → ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ↔ ∃ 𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
39	38	ibi	⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } → ∃ 𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
40		ssid	⊢ ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑦 )
41		fveq2	⊢ ( 𝑥 = 𝑦 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) )
42	41	sseq1d	⊢ ( 𝑥 = 𝑦 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑦 ) ) )
43	42	rspcev	⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
44	40 43	mpan2	⊢ ( 𝑦 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
45		iinss	⊢ ( ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
46	44 45	syl	⊢ ( 𝑦 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
47		sseq1	⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
48	46 47	syl5ib	⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ( 𝑦 ∈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
49	48	ralrimiv	⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
50	49	reximi	⊢ ( ∃ 𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
51	24 33 39 50	4syl	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
52		rabn0	⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
53	51 52	sylibr	⊢ ( 𝐴 ≠ ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ )
54	53	necon4i	⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ → 𝐴 = ∅ )
55	3 54	impbii	⊢ ( 𝐴 = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )