Theorem scottabf 9910

Description: Value of the Scott operation at a class abstraction. Variant of scottab 9911 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 9900	. 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 1947	. . . . . . 7 ⊢ Ⅎ𝑥(rank‘𝑧) ⊆ (rank‘𝑤)
7	5, 6	nfralw 3309	. . . . . 6 ⊢ Ⅎ𝑥∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)
8	4, 7	nfan 1932	. . . . 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 6877	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑥) = (rank‘𝑧))
23		simpr 490	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
24	23	fveq2d 6877	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑦) = (rank‘𝑤))
25	22, 24	sseq12d 3963	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑤)))
26	20, 25	imbi12d 347	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))))
27	26	cbvaldvaw 2071	. . . . . . 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 1832	. 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 1568   = wceq 1570  Ⅎwnf 1816  [wsb 2099   ∈ wcel 2145  {cab 2738  ∀wral 3076  {crab 3412   ⊆ wss 3898  ‘cfv 6527  rankcrnk 9745  Scott cscott 9899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-scott 9900

This theorem is used by:  scottab  9911  scottabes  9912