Theorem ecscottd

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

	Ref	Expression
Hypotheses	ecscottd.1	⊢ ( 𝜑 → 𝑅 Er 𝑉 )
	ecscottd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	ecscottd	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ Scott [ 𝐴 ] 𝑅 = Scott [ 𝐵 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ecscottd.1	⊢ ( 𝜑 → 𝑅 Er 𝑉 )
2		ecscottd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3	1 2	erscottd	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 𝑅 𝐵 ↔ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) )
5		dfec2	⊢ ( 𝐴 ∈ 𝑉 → [ 𝐴 ] 𝑅 = { 𝑥 ∣ 𝐴 𝑅 𝑥 } )
6	2 5	syl	⊢ ( 𝜑 → [ 𝐴 ] 𝑅 = { 𝑥 ∣ 𝐴 𝑅 𝑥 } )
7	1	ersymb	⊢ ( 𝜑 → ( 𝐴 𝑅 𝑥 ↔ 𝑥 𝑅 𝐴 ) )
8	7	abbidv	⊢ ( 𝜑 → { 𝑥 ∣ 𝐴 𝑅 𝑥 } = { 𝑥 ∣ 𝑥 𝑅 𝐴 } )
9	6 8	eqtrd	⊢ ( 𝜑 → [ 𝐴 ] 𝑅 = { 𝑥 ∣ 𝑥 𝑅 𝐴 } )
10	9	scotteqd	⊢ ( 𝜑 → Scott [ 𝐴 ] 𝑅 = Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑉 ) → Scott [ 𝐴 ] 𝑅 = Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } )
12		dfec2	⊢ ( 𝐵 ∈ 𝑉 → [ 𝐵 ] 𝑅 = { 𝑥 ∣ 𝐵 𝑅 𝑥 } )
13	1	ersymb	⊢ ( 𝜑 → ( 𝐵 𝑅 𝑥 ↔ 𝑥 𝑅 𝐵 ) )
14	13	abbidv	⊢ ( 𝜑 → { 𝑥 ∣ 𝐵 𝑅 𝑥 } = { 𝑥 ∣ 𝑥 𝑅 𝐵 } )
15	12 14	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑉 ) → [ 𝐵 ] 𝑅 = { 𝑥 ∣ 𝑥 𝑅 𝐵 } )
16	15	scotteqd	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑉 ) → Scott [ 𝐵 ] 𝑅 = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } )
17	11 16	eqeq12d	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑉 ) → ( Scott [ 𝐴 ] 𝑅 = Scott [ 𝐵 ] 𝑅 ↔ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) )
18	4 17	bitr4d	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 𝑅 𝐵 ↔ Scott [ 𝐴 ] 𝑅 = Scott [ 𝐵 ] 𝑅 ) )
19	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝑅 Er 𝑉 )
20		simpr	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 𝑅 𝐵 )
21	19 20	ercl2	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐵 ∈ 𝑉 )
22	21	stoic1a	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑉 ) → ¬ 𝐴 𝑅 𝐵 )
23		erdm	⊢ ( 𝑅 Er 𝑉 → dom 𝑅 = 𝑉 )
24	1 23	syl	⊢ ( 𝜑 → dom 𝑅 = 𝑉 )
25	2 24	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )
26		ecdmn0	⊢ ( 𝐴 ∈ dom 𝑅 ↔ [ 𝐴 ] 𝑅 ≠ ∅ )
27	25 26	sylib	⊢ ( 𝜑 → [ 𝐴 ] 𝑅 ≠ ∅ )
28		scott0b	⊢ ( [ 𝐴 ] 𝑅 = ∅ ↔ Scott [ 𝐴 ] 𝑅 = ∅ )
29	28	necon3bii	⊢ ( [ 𝐴 ] 𝑅 ≠ ∅ ↔ Scott [ 𝐴 ] 𝑅 ≠ ∅ )
30	27 29	sylib	⊢ ( 𝜑 → Scott [ 𝐴 ] 𝑅 ≠ ∅ )
31	30	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑉 ) → Scott [ 𝐴 ] 𝑅 ≠ ∅ )
32	24	eleq2d	⊢ ( 𝜑 → ( 𝐵 ∈ dom 𝑅 ↔ 𝐵 ∈ 𝑉 ) )
33	32	notbid	⊢ ( 𝜑 → ( ¬ 𝐵 ∈ dom 𝑅 ↔ ¬ 𝐵 ∈ 𝑉 ) )
34	33	biimpar	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑉 ) → ¬ 𝐵 ∈ dom 𝑅 )
35		ecdmn0	⊢ ( 𝐵 ∈ dom 𝑅 ↔ [ 𝐵 ] 𝑅 ≠ ∅ )
36	35	necon2bbii	⊢ ( [ 𝐵 ] 𝑅 = ∅ ↔ ¬ 𝐵 ∈ dom 𝑅 )
37	34 36	sylibr	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑉 ) → [ 𝐵 ] 𝑅 = ∅ )
38		scott0b	⊢ ( [ 𝐵 ] 𝑅 = ∅ ↔ Scott [ 𝐵 ] 𝑅 = ∅ )
39	37 38	sylib	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑉 ) → Scott [ 𝐵 ] 𝑅 = ∅ )
40	31 39	neeqtrrd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑉 ) → Scott [ 𝐴 ] 𝑅 ≠ Scott [ 𝐵 ] 𝑅 )
41	40	neneqd	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑉 ) → ¬ Scott [ 𝐴 ] 𝑅 = Scott [ 𝐵 ] 𝑅 )
42	22 41	2falsed	⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ 𝑉 ) → ( 𝐴 𝑅 𝐵 ↔ Scott [ 𝐴 ] 𝑅 = Scott [ 𝐵 ] 𝑅 ) )
43	18 42	pm2.61dan	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ Scott [ 𝐴 ] 𝑅 = Scott [ 𝐵 ] 𝑅 ) )