Theorem scottabf 42989

Description: Value of the Scott operation at a class abstraction. Variant of scottab 42990 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 42985	. 2 ⊢ Scott {𝑥 ∣ 𝜑} = {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)}
2		df-rab 3433	. 2 ⊢ {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)} = {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))}
3		eqabcb 2875	. . 3 ⊢ ({𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ ∀𝑧((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}))
4		nfsab1 2717	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑥 ∣ 𝜑}
5		nfab1 2905	. . . . . . 7 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
6		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑥(rank‘𝑧) ⊆ (rank‘𝑤)
7	5, 6	nfralw 3308	. . . . . 6 ⊢ Ⅎ𝑥∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)
8	4, 7	nfan 1902	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))
9		vex 3478	. . . . 5 ⊢ 𝑧 ∈ V
10		abid 2713	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
11		eleq1w 2816	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ 𝜑}))
12	10, 11	bitr3id 284	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝑧 ∈ {𝑥 ∣ 𝜑}))
13		df-clab 2710	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
14		scottabf.1	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝜓
15		scottabf.2	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
16	14, 15	sbiev 2308	. . . . . . . . . . . 12 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
17	13, 16	bitr2i 275	. . . . . . . . . . 11 ⊢ (𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})
18		eleq1w 2816	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
19	17, 18	bitrid 282	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
20	19	adantl 482	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
21		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧)
22	21	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑥) = (rank‘𝑧))
23		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
24	23	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑦) = (rank‘𝑤))
25	22, 24	sseq12d 4015	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑤)))
26	20, 25	imbi12d 344	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))))
27	26	cbvaldvaw 2041	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))))
28		df-ral 3062	. . . . . . 7 ⊢ (∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤)))
29	27, 28	bitr4di 288	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)))
30	12, 29	anbi12d 631	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))))
31	8, 9, 30	elabf 3665	. . . 4 ⊢ (𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)))
32	31	bicomi 223	. . 3 ⊢ ((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
33	3, 32	mpgbir 1801	. 2 ⊢ {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
34	1, 2, 33	3eqtri 2764	1 ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541  Ⅎwnf 1785  [wsb 2067   ∈ wcel 2106  {cab 2709  ∀wral 3061  {crab 3432   ⊆ wss 3948  ‘cfv 6543  rankcrnk 9757  Scott cscott 42984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-scott 42985

This theorem is referenced by:  scottab  42990  scottabes  42991