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 ) ) )