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