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 
|- ( ph -> .~ Er V )
ercpbl.v 
|- ( ph -> V e. W )
ercpbl.f 
|- F = ( x e. V |-> [ x ] .~ )
erlecpbl.e 
|- ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A N B <-> C N D ) ) )
Assertion erlecpbl 
|- ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( A N B <-> C N D ) ) )

Proof

Step Hyp Ref Expression
1 ercpbl.r 
 |-  ( ph -> .~ Er V )
2 ercpbl.v 
 |-  ( ph -> V e. W )
3 ercpbl.f 
 |-  F = ( x e. V |-> [ x ] .~ )
4 erlecpbl.e 
 |-  ( ph -> ( ( A .~ C /\ B .~ D ) -> ( A N B <-> C N D ) ) )
5 1 3ad2ant1 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> .~ Er V )
6 2 3ad2ant1 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> V e. W )
7 simp2l 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> A e. V )
8 5 6 3 7 ercpbllem 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( F ` A ) = ( F ` C ) <-> A .~ C ) )
9 simp2r 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> B e. V )
10 5 6 3 9 ercpbllem 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( F ` B ) = ( F ` D ) <-> B .~ D ) )
11 8 10 anbi12d 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) <-> ( A .~ C /\ B .~ D ) ) )
12 4 3ad2ant1 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .~ C /\ B .~ D ) -> ( A N B <-> C N D ) ) )
13 11 12 sylbid 
 |-  ( ( ph /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( ( F ` A ) = ( F ` C ) /\ ( F ` B ) = ( F ` D ) ) -> ( A N B <-> C N D ) ) )