This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) → ( 𝐴 𝑁 𝐵 ↔ 𝐶 𝑁 𝐷 ) ) )