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)

	Ref	Expression
Hypotheses	ercpbl.r	|- ( ph -> .~ Er V )
	ercpbl.v	|- ( ph -> V e. _V )
	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. _V )
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. _V )
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 ) ) )