Theorem scottabf

Description: Value of the Scott operation at a class abstraction. Variant of scottab with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023)

	Ref	Expression
Hypotheses	scottabf.1	⊢ Ⅎ 𝑥 𝜓
	scottabf.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	scottabf	⊢ Scott { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }

Proof

Step	Hyp	Ref	Expression
1		scottabf.1	⊢ Ⅎ 𝑥 𝜓
2		scottabf.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3		df-scott	⊢ Scott { 𝑥 ∣ 𝜑 } = { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) }
4		df-rab	⊢ { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) } = { 𝑧 ∣ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) }
5		eqabcb	⊢ ( { 𝑧 ∣ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ↔ ∀ 𝑧 ( ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) ↔ 𝑧 ∈ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ) )
6		nfsab1	⊢ Ⅎ 𝑥 𝑧 ∈ { 𝑥 ∣ 𝜑 }
7		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
8		nfv	⊢ Ⅎ 𝑥 ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 )
9	7 8	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 )
10	6 9	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) )
11		vex	⊢ 𝑧 ∈ V
12		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
13		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) )
14	12 13	bitr3id	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) )
15		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
16	1 2	sbiev	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
17	15 16	bitr2i	⊢ ( 𝜓 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
18		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ) )
19	17 18	bitrid	⊢ ( 𝑦 = 𝑤 → ( 𝜓 ↔ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ) )
20	19	adantl	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜓 ↔ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ) )
21		simpl	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑥 = 𝑧 )
22	21	fveq2d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑧 ) )
23		simpr	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
24	23	fveq2d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( rank ‘ 𝑦 ) = ( rank ‘ 𝑤 ) )
25	22 24	sseq12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) )
26	20 25	imbi12d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑤 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) ) )
27	26	cbvaldvaw	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑤 ( 𝑤 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) ) )
28		df-ral	⊢ ( ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ↔ ∀ 𝑤 ( 𝑤 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) )
29	27 28	bitr4di	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) )
30	14 29	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) ) )
31	10 11 30	elabf	⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ↔ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) )
32	31	bicomi	⊢ ( ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) ↔ 𝑧 ∈ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } )
33	5 32	mpgbir	⊢ { 𝑧 ∣ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑤 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑤 ) ) } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
34	3 4 33	3eqtri	⊢ Scott { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( 𝜓 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }