Theorem scottabf 41858

Description: Value of the Scott operation at a class abstraction. Variant of scottab 41859 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 41854	. 2 ⊢ Scott {𝑥 ∣ 𝜑} = {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)}
2		df-rab 3073	. 2 ⊢ {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)} = {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))}
3		abeq1 2873	. . 3 ⊢ ({𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ ∀𝑧((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}))
4		nfsab1 2723	. . . . . 6 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑥 ∣ 𝜑}
5		nfab1 2909	. . . . . . 7 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
6		nfv 1917	. . . . . . 7 ⊢ Ⅎ𝑥(rank‘𝑧) ⊆ (rank‘𝑤)
7	5, 6	nfralw 3151	. . . . . 6 ⊢ Ⅎ𝑥∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)
8	4, 7	nfan 1902	. . . . 5 ⊢ Ⅎ𝑥(𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))
9		vex 3436	. . . . 5 ⊢ 𝑧 ∈ V
10		abid 2719	. . . . . . 7 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
11		eleq1w 2821	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ 𝜑}))
12	10, 11	bitr3id 285	. . . . . 6 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝑧 ∈ {𝑥 ∣ 𝜑}))
13		df-clab 2716	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
14		scottabf.1	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝜓
15		scottabf.2	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
16	14, 15	sbiev 2309	. . . . . . . . . . . 12 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
17	13, 16	bitr2i 275	. . . . . . . . . . 11 ⊢ (𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜑})
18		eleq1w 2821	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
19	17, 18	syl5bb 283	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
20	19	adantl 482	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑}))
21		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧)
22	21	fveq2d 6778	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑥) = (rank‘𝑧))
23		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
24	23	fveq2d 6778	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑦) = (rank‘𝑤))
25	22, 24	sseq12d 3954	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑤)))
26	20, 25	imbi12d 345	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))))
27	26	cbvaldvaw 2041	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))))
28		df-ral 3069	. . . . . . 7 ⊢ (∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤)))
29	27, 28	bitr4di 289	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)))
30	12, 29	anbi12d 631	. . . . 5 ⊢ (𝑥 = 𝑧 → ((𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))))
31	8, 9, 30	elabf 3606	. . . 4 ⊢ (𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)))
32	31	bicomi 223	. . 3 ⊢ ((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
33	3, 32	mpgbir 1802	. 2 ⊢ {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
34	1, 2, 33	3eqtri 2770	1 ⊢ Scott {𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539  Ⅎwnf 1786  [wsb 2067   ∈ wcel 2106  {cab 2715  ∀wral 3064  {crab 3068   ⊆ wss 3887  ‘cfv 6433  rankcrnk 9521  Scott cscott 41853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-scott 41854

This theorem is referenced by:  scottab  41859  scottabes  41860