Theorem erscottd

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

	Ref	Expression
Hypotheses	erscottd.1	⊢ ( 𝜑 → 𝑅 Er 𝑉 )
	erscottd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	erscottd	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		erscottd.1	⊢ ( 𝜑 → 𝑅 Er 𝑉 )
2		erscottd.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ∧ 𝑥 𝑅 𝐴 ) → 𝑅 Er 𝑉 )
4		simp3	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ∧ 𝑥 𝑅 𝐴 ) → 𝑥 𝑅 𝐴 )
5		simp2	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ∧ 𝑥 𝑅 𝐴 ) → 𝐴 𝑅 𝐵 )
6	3 4 5	ertrd	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ∧ 𝑥 𝑅 𝐴 ) → 𝑥 𝑅 𝐵 )
7	6	3expia	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝑥 𝑅 𝐴 → 𝑥 𝑅 𝐵 ) )
8	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ∧ 𝑥 𝑅 𝐵 ) → 𝑅 Er 𝑉 )
9		simp3	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ∧ 𝑥 𝑅 𝐵 ) → 𝑥 𝑅 𝐵 )
10		simp2	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ∧ 𝑥 𝑅 𝐵 ) → 𝐴 𝑅 𝐵 )
11	8 9 10	ertr4d	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ∧ 𝑥 𝑅 𝐵 ) → 𝑥 𝑅 𝐴 )
12	11	3expia	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝑥 𝑅 𝐵 → 𝑥 𝑅 𝐴 ) )
13	7 12	impbid	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → ( 𝑥 𝑅 𝐴 ↔ 𝑥 𝑅 𝐵 ) )
14	13	abbidv	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → { 𝑥 ∣ 𝑥 𝑅 𝐴 } = { 𝑥 ∣ 𝑥 𝑅 𝐵 } )
15	14	scotteqd	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } )
16	1 2	erref	⊢ ( 𝜑 → 𝐴 𝑅 𝐴 )
17		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝐴 ↔ 𝐴 𝑅 𝐴 ) )
18	2 16 17	elabd	⊢ ( 𝜑 → 𝐴 ∈ { 𝑥 ∣ 𝑥 𝑅 𝐴 } )
19		n0i	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝑥 𝑅 𝐴 } → ¬ { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ )
20	18 19	syl	⊢ ( 𝜑 → ¬ { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ )
21		scott0b	⊢ ( { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ ↔ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ )
22	20 21	sylnib	⊢ ( 𝜑 → ¬ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ )
23		disjeq0	⊢ ( ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∩ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) = ∅ → ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ↔ ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ ∧ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } = ∅ ) ) )
24	23	biimpcd	⊢ ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } → ( ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∩ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) = ∅ → ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ ∧ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } = ∅ ) ) )
25		simpl	⊢ ( ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ ∧ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } = ∅ ) → Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ )
26	25	con3i	⊢ ( ¬ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ → ¬ ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ ∧ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } = ∅ ) )
27	24 26	nsyli	⊢ ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } → ( ¬ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ → ¬ ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∩ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) = ∅ ) )
28		df-ne	⊢ ( ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∩ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) ≠ ∅ ↔ ¬ ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∩ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) = ∅ )
29		ndisj	⊢ ( ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∩ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) ≠ ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) )
30	28 29	bitr3i	⊢ ( ¬ ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∩ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) )
31	27 30	imbitrdi	⊢ ( Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } → ( ¬ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = ∅ → ∃ 𝑦 ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) ) )
32	22 31	mpan9	⊢ ( ( 𝜑 ∧ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → ∃ 𝑦 ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) )
33	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → 𝑅 Er 𝑉 )
34		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝐴 ↔ 𝑦 𝑅 𝐴 ) )
35	34	elscottab	⊢ ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } → 𝑦 𝑅 𝐴 )
36	35	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → 𝑦 𝑅 𝐴 )
37		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝑅 𝐵 ↔ 𝑦 𝑅 𝐵 ) )
38	37	elscottab	⊢ ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } → 𝑦 𝑅 𝐵 )
39	38	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → 𝑦 𝑅 𝐵 )
40	33 36 39	ertr3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → 𝐴 𝑅 𝐵 )
41	40	3expib	⊢ ( 𝜑 → ( ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → 𝐴 𝑅 𝐵 ) )
42	41	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → 𝐴 𝑅 𝐵 ) )
43	42	adantr	⊢ ( ( 𝜑 ∧ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → ( ∃ 𝑦 ( 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } ∧ 𝑦 ∈ Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → 𝐴 𝑅 𝐵 ) )
44	32 43	mpd	⊢ ( ( 𝜑 ∧ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) → 𝐴 𝑅 𝐵 )
45	15 44	impbida	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ Scott { 𝑥 ∣ 𝑥 𝑅 𝐴 } = Scott { 𝑥 ∣ 𝑥 𝑅 𝐵 } ) )