Theorem erlecpbl

Description: Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by AV, 12-Jul-2024)

	Ref	Expression
Hypotheses	ercpbl.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
	ercpbl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
	ercpbl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
	erlecpbl.e	⊢ ( 𝜑 → ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 𝑁 𝐵 ↔ 𝐶 𝑁 𝐷 ) ) )
Assertion	erlecpbl	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) → ( 𝐴 𝑁 𝐵 ↔ 𝐶 𝑁 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ercpbl.r	⊢ ( 𝜑 → ∼ Er 𝑉 )
2		ercpbl.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
3		ercpbl.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
4		erlecpbl.e	⊢ ( 𝜑 → ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 𝑁 𝐵 ↔ 𝐶 𝑁 𝐷 ) ) )
5	1	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ∼ Er 𝑉 )
6	2	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝑉 ∈ 𝑊 )
7		simp2l	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
8	5 6 3 7	ercpbllem	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐴 ∼ 𝐶 ) )
9		simp2r	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
10	5 6 3 9	ercpbllem	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ↔ 𝐵 ∼ 𝐷 ) )
11	8 10	anbi12d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) ↔ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) )
12	4	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 𝑁 𝐵 ↔ 𝐶 𝑁 𝐷 ) ) )
13	11 12	sylbid	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) → ( 𝐴 𝑁 𝐵 ↔ 𝐶 𝑁 𝐷 ) ) )