ecscottd

Description: Applying the Scott operation to equivalence classes preserves their equality property. (Contributed by BTernaryTau, 20-Oct-2026)

	Ref	Expression
Hypotheses	ecscottd.1	$⊢ φ \to R Er V$
	ecscottd.2	$⊢ φ \to A \in V$
Assertion	ecscottd	$⊢ φ \to (A R B \leftrightarrow Scott [A] R = Scott [B] R)$

Proof

Step	Hyp	Ref	Expression
1		ecscottd.1	$⊢ φ \to R Er V$
2		ecscottd.2	$⊢ φ \to A \in V$
3	1 2	erscottd	$⊢ φ \to (A R B \leftrightarrow Scott \{x \| x R A\} = Scott \{x \| x R B\})$
4	3	adantr	$⊢ (φ \land B \in V) \to (A R B \leftrightarrow Scott \{x \| x R A\} = Scott \{x \| x R B\})$
5		dfec2	$⊢ A \in V \to [A] R = \{x \| A R x\}$
6	2 5	syl	$⊢ φ \to [A] R = \{x \| A R x\}$
7	1	ersymb	$⊢ φ \to (A R x \leftrightarrow x R A)$
8	7	abbidv	$⊢ φ \to \{x \| A R x\} = \{x \| x R A\}$
9	6 8	eqtrd	$⊢ φ \to [A] R = \{x \| x R A\}$
10	9	scotteqd	$⊢ φ \to Scott [A] R = Scott \{x \| x R A\}$
11	10	adantr	$⊢ (φ \land B \in V) \to Scott [A] R = Scott \{x \| x R A\}$
12		dfec2	$⊢ B \in V \to [B] R = \{x \| B R x\}$
13	1	ersymb	$⊢ φ \to (B R x \leftrightarrow x R B)$
14	13	abbidv	$⊢ φ \to \{x \| B R x\} = \{x \| x R B\}$
15	12 14	sylan9eqr	$⊢ (φ \land B \in V) \to [B] R = \{x \| x R B\}$
16	15	scotteqd	$⊢ (φ \land B \in V) \to Scott [B] R = Scott \{x \| x R B\}$
17	11 16	eqeq12d	$⊢ (φ \land B \in V) \to (Scott [A] R = Scott [B] R \leftrightarrow Scott \{x \| x R A\} = Scott \{x \| x R B\})$
18	4 17	bitr4d	$⊢ (φ \land B \in V) \to (A R B \leftrightarrow Scott [A] R = Scott [B] R)$
19	1	adantr	$⊢ (φ \land A R B) \to R Er V$
20		simpr	$⊢ (φ \land A R B) \to A R B$
21	19 20	ercl2	$⊢ (φ \land A R B) \to B \in V$
22	21	stoic1a	$⊢ (φ \land \neg B \in V) \to \neg A R B$
23		erdm	$⊢ R Er V \to dom R = V$
24	1 23	syl	$⊢ φ \to dom R = V$
25	2 24	eleqtrrd	$⊢ φ \to A \in dom R$
26		ecdmn0	$⊢ A \in dom R \leftrightarrow [A] R \neq \emptyset$
27	25 26	sylib	$⊢ φ \to [A] R \neq \emptyset$
28		scott0b	$⊢ [A] R = \emptyset \leftrightarrow Scott [A] R = \emptyset$
29	28	necon3bii	$⊢ [A] R \neq \emptyset \leftrightarrow Scott [A] R \neq \emptyset$
30	27 29	sylib	$⊢ φ \to Scott [A] R \neq \emptyset$
31	30	adantr	$⊢ (φ \land \neg B \in V) \to Scott [A] R \neq \emptyset$
32	24	eleq2d	$⊢ φ \to (B \in dom R \leftrightarrow B \in V)$
33	32	notbid	$⊢ φ \to (\neg B \in dom R \leftrightarrow \neg B \in V)$
34	33	biimpar	$⊢ (φ \land \neg B \in V) \to \neg B \in dom R$
35		ecdmn0	$⊢ B \in dom R \leftrightarrow [B] R \neq \emptyset$
36	35	necon2bbii	$⊢ [B] R = \emptyset \leftrightarrow \neg B \in dom R$
37	34 36	sylibr	$⊢ (φ \land \neg B \in V) \to [B] R = \emptyset$
38		scott0b	$⊢ [B] R = \emptyset \leftrightarrow Scott [B] R = \emptyset$
39	37 38	sylib	$⊢ (φ \land \neg B \in V) \to Scott [B] R = \emptyset$
40	31 39	neeqtrrd	$⊢ (φ \land \neg B \in V) \to Scott [A] R \neq Scott [B] R$
41	40	neneqd	$⊢ (φ \land \neg B \in V) \to \neg Scott [A] R = Scott [B] R$
42	22 41	2falsed	$⊢ (φ \land \neg B \in V) \to (A R B \leftrightarrow Scott [A] R = Scott [B] R)$
43	18 42	pm2.61dan	$⊢ φ \to (A R B \leftrightarrow Scott [A] R = Scott [B] R)$

Metamath Proof Explorer

Theorem ecscottd

Proof