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 ) = (/) ) ) )