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

Metamath Proof Explorer

Theorem disjecxrncnvep

Description: Two ways of saying that cosets are disjoint, special case of disjecxrn . (Contributed by Peter Mazsa, 12-Jul-2020) (Revised by Peter Mazsa, 25-Aug-2023)

Ref Expression
Assertion disjecxrncnvep 
|- ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. `' _E ) i^i [ B ] ( R |X. `' _E ) ) = (/) <-> ( ( A i^i B ) = (/) \/ ( [ A ] R i^i [ B ] R ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 disjecxrn 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. `' _E ) i^i [ B ] ( R |X. `' _E ) ) = (/) <-> ( ( [ A ] R i^i [ B ] R ) = (/) \/ ( [ A ] `' _E i^i [ B ] `' _E ) = (/) ) ) )
2 orcom 
 |-  ( ( ( [ A ] R i^i [ B ] R ) = (/) \/ ( [ A ] `' _E i^i [ B ] `' _E ) = (/) ) <-> ( ( [ A ] `' _E i^i [ B ] `' _E ) = (/) \/ ( [ A ] R i^i [ B ] R ) = (/) ) )
3 1 2 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. `' _E ) i^i [ B ] ( R |X. `' _E ) ) = (/) <-> ( ( [ A ] `' _E i^i [ B ] `' _E ) = (/) \/ ( [ A ] R i^i [ B ] R ) = (/) ) ) )
4 disjeccnvep 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] `' _E i^i [ B ] `' _E ) = (/) <-> ( A i^i B ) = (/) ) )
5 4 orbi1d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ( [ A ] `' _E i^i [ B ] `' _E ) = (/) \/ ( [ A ] R i^i [ B ] R ) = (/) ) <-> ( ( A i^i B ) = (/) \/ ( [ A ] R i^i [ B ] R ) = (/) ) ) )
6 3 5 bitrd 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. `' _E ) i^i [ B ] ( R |X. `' _E ) ) = (/) <-> ( ( A i^i B ) = (/) \/ ( [ A ] R i^i [ B ] R ) = (/) ) ) )