Theorem scottabf 9939

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

Hypotheses

Ref	Expression
scottabf.1	⊢ Ⅎ𝑥𝜓
scottabf.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
scottabf	⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}

Distinct variable groups:   𝜑,𝑦   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥, 𝑦)

Proof of Theorem scottabf

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-scott 9929	. 2 ⊢ Scott {𝑥 ∣ 𝜑} = {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)}
2		df-rab 3413	. 2 ⊢ {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)} = {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))}
3		eqabcb 2900	. . 3 ⊢ ({𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ ∀𝑧((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}))
4		nfsab1 2746	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑥 ∣ 𝜑}
5		nfab1 2924	. . . . . . 7 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
6		nfv 1946	. . . . . . 7 ⊢ Ⅎ𝑥(rank‘𝑧) ⊆ (rank‘𝑤)
7	5, 6	nfralw 3309	. . . . . 6 ⊢ Ⅎ𝑥∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)
8	4, 7	nfan 1931	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))
9		vex 3454	. . . . 5 ⊢ 𝑧 ∈ V
10		abid 2742	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
11		eleq1w 2843	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ 𝜑}))
12	10, 11	bitr3id 288	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝑧 ∈ {𝑥 ∣ 𝜑}))
13		df-clab 2739	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
14		scottabf.1	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝜓
15		scottabf.2	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
16	14, 15	sbiev 2345	. . . . . . . . . . . 12 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
17	13, 16	bitr2i 279	. . . . . . . . . . 11 ⊢ (𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})
18		eleq1w 2843	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
19	17, 18	bitrid 286	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
20	19	adantl 487	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
21		simpl 488	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧)
22	21	fveq2d 6889	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑥) = (rank‘𝑧))
23		simpr 490	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
24	23	fveq2d 6889	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑦) = (rank‘𝑤))
25	22, 24	sseq12d 3941	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑤)))
26	20, 25	imbi12d 347	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))))
27	26	cbvaldvaw 2070	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))))
28		df-ral 3077	. . . . . . 7 ⊢ (∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤)))
29	27, 28	bitr4di 292	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)))
30	12, 29	anbi12d 644	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))))
31	8, 9, 30	elabf 3628	. . . 4 ⊢ (𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)))
32	31	bicomi 227	. . 3 ⊢ ((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
33	3, 32	mpgbir 1831	. 2 ⊢ {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
34	1, 2, 33	3eqtri 2787	1 ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  Ⅎwnf 1815  [wsb 2098   ∈ wcel 2144  {cab 2738  ∀wral 3076  {crab 3412   ⊆ wss 3895  ‘cfv 6538  rankcrnk 9767  Scott cscott 9928

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-scott 9929

This theorem is used by:  scottab  9940  scottabes  9941