erscottd

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

	Ref	Expression
Hypotheses	erscottd.1	$⊢ φ \to R Er V$
	erscottd.2	$⊢ φ \to A \in V$
Assertion	erscottd	$⊢ φ \to (A R B \leftrightarrow Scott \{x \| x R A\} = Scott \{x \| x R B\})$

Proof

Step	Hyp	Ref	Expression
1		erscottd.1	$⊢ φ \to R Er V$
2		erscottd.2	$⊢ φ \to A \in V$
3	1	3ad2ant1	$⊢ (φ \land A R B \land x R A) \to R Er V$
4		simp3	$⊢ (φ \land A R B \land x R A) \to x R A$
5		simp2	$⊢ (φ \land A R B \land x R A) \to A R B$
6	3 4 5	ertrd	$⊢ (φ \land A R B \land x R A) \to x R B$
7	6	3expia	$⊢ (φ \land A R B) \to (x R A \to x R B)$
8	1	3ad2ant1	$⊢ (φ \land A R B \land x R B) \to R Er V$
9		simp3	$⊢ (φ \land A R B \land x R B) \to x R B$
10		simp2	$⊢ (φ \land A R B \land x R B) \to A R B$
11	8 9 10	ertr4d	$⊢ (φ \land A R B \land x R B) \to x R A$
12	11	3expia	$⊢ (φ \land A R B) \to (x R B \to x R A)$
13	7 12	impbid	$⊢ (φ \land A R B) \to (x R A \leftrightarrow x R B)$
14	13	abbidv	$⊢ (φ \land A R B) \to \{x \| x R A\} = \{x \| x R B\}$
15	14	scotteqd	$⊢ (φ \land A R B) \to Scott \{x \| x R A\} = Scott \{x \| x R B\}$
16	1 2	erref	$⊢ φ \to A R A$
17		breq1	$⊢ x = A \to (x R A \leftrightarrow A R A)$
18	2 16 17	elabd	$⊢ φ \to A \in \{x \| x R A\}$
19		n0i	$⊢ A \in \{x \| x R A\} \to \neg \{x \| x R A\} = \emptyset$
20	18 19	syl	$⊢ φ \to \neg \{x \| x R A\} = \emptyset$
21		scott0b	$⊢ \{x \| x R A\} = \emptyset \leftrightarrow Scott \{x \| x R A\} = \emptyset$
22	20 21	sylnib	$⊢ φ \to \neg Scott \{x \| x R A\} = \emptyset$
23		disjeq0	$⊢ Scott \{x \| x R A\} \cap Scott \{x \| x R B\} = \emptyset \to (Scott \{x \| x R A\} = Scott \{x \| x R B\} \leftrightarrow (Scott \{x \| x R A\} = \emptyset \land Scott \{x \| x R B\} = \emptyset))$
24	23	biimpcd	$⊢ Scott \{x \| x R A\} = Scott \{x \| x R B\} \to (Scott \{x \| x R A\} \cap Scott \{x \| x R B\} = \emptyset \to (Scott \{x \| x R A\} = \emptyset \land Scott \{x \| x R B\} = \emptyset))$
25		simpl	$⊢ (Scott \{x \| x R A\} = \emptyset \land Scott \{x \| x R B\} = \emptyset) \to Scott \{x \| x R A\} = \emptyset$
26	25	con3i	$⊢ \neg Scott \{x \| x R A\} = \emptyset \to \neg (Scott \{x \| x R A\} = \emptyset \land Scott \{x \| x R B\} = \emptyset)$
27	24 26	nsyli	$⊢ Scott \{x \| x R A\} = Scott \{x \| x R B\} \to (\neg Scott \{x \| x R A\} = \emptyset \to \neg Scott \{x \| x R A\} \cap Scott \{x \| x R B\} = \emptyset)$
28		df-ne	$⊢ Scott \{x \| x R A\} \cap Scott \{x \| x R B\} \neq \emptyset \leftrightarrow \neg Scott \{x \| x R A\} \cap Scott \{x \| x R B\} = \emptyset$
29		ndisj	$⊢ Scott \{x \| x R A\} \cap Scott \{x \| x R B\} \neq \emptyset \leftrightarrow \exists y (y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\})$
30	28 29	bitr3i	$⊢ \neg Scott \{x \| x R A\} \cap Scott \{x \| x R B\} = \emptyset \leftrightarrow \exists y (y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\})$
31	27 30	imbitrdi	$⊢ Scott \{x \| x R A\} = Scott \{x \| x R B\} \to (\neg Scott \{x \| x R A\} = \emptyset \to \exists y (y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\}))$
32	22 31	mpan9	$⊢ (φ \land Scott \{x \| x R A\} = Scott \{x \| x R B\}) \to \exists y (y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\})$
33	1	3ad2ant1	$⊢ (φ \land y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\}) \to R Er V$
34		breq1	$⊢ x = y \to (x R A \leftrightarrow y R A)$
35	34	elscottab	$⊢ y \in Scott \{x \| x R A\} \to y R A$
36	35	3ad2ant2	$⊢ (φ \land y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\}) \to y R A$
37		breq1	$⊢ x = y \to (x R B \leftrightarrow y R B)$
38	37	elscottab	$⊢ y \in Scott \{x \| x R B\} \to y R B$
39	38	3ad2ant3	$⊢ (φ \land y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\}) \to y R B$
40	33 36 39	ertr3d	$⊢ (φ \land y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\}) \to A R B$
41	40	3expib	$⊢ φ \to ((y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\}) \to A R B)$
42	41	exlimdv	$⊢ φ \to (\exists y (y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\}) \to A R B)$
43	42	adantr	$⊢ (φ \land Scott \{x \| x R A\} = Scott \{x \| x R B\}) \to (\exists y (y \in Scott \{x \| x R A\} \land y \in Scott \{x \| x R B\}) \to A R B)$
44	32 43	mpd	$⊢ (φ \land Scott \{x \| x R A\} = Scott \{x \| x R B\}) \to A R B$
45	15 44	impbida	$⊢ φ \to (A R B \leftrightarrow Scott \{x \| x R A\} = Scott \{x \| x R B\})$

Metamath Proof Explorer

Theorem erscottd

Proof