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

Metamath Proof Explorer

Theorem disjecxrn

Description: Two ways of saying that ( R |X. S ) -cosets are disjoint. (Contributed by Peter Mazsa, 19-Jun-2020) (Revised by Peter Mazsa, 21-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 ecxrn 
 |-  ( A e. V -> [ A ] ( R |X. S ) = { <. y , z >. | ( A R y /\ A S z ) } )
2 ecxrn 
 |-  ( B e. W -> [ B ] ( R |X. S ) = { <. y , z >. | ( B R y /\ B S z ) } )
3 1 2 ineqan12d 
 |-  ( ( A e. V /\ B e. W ) -> ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) = ( { <. y , z >. | ( A R y /\ A S z ) } i^i { <. y , z >. | ( B R y /\ B S z ) } ) )
4 inopab 
 |-  ( { <. y , z >. | ( A R y /\ A S z ) } i^i { <. y , z >. | ( B R y /\ B S z ) } ) = { <. y , z >. | ( ( A R y /\ A S z ) /\ ( B R y /\ B S z ) ) }
5 3 4 eqtrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) = { <. y , z >. | ( ( A R y /\ A S z ) /\ ( B R y /\ B S z ) ) } )
6 an4 
 |-  ( ( ( A R y /\ A S z ) /\ ( B R y /\ B S z ) ) <-> ( ( A R y /\ B R y ) /\ ( A S z /\ B S z ) ) )
7 6 opabbii 
 |-  { <. y , z >. | ( ( A R y /\ A S z ) /\ ( B R y /\ B S z ) ) } = { <. y , z >. | ( ( A R y /\ B R y ) /\ ( A S z /\ B S z ) ) }
8 5 7 eqtrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) = { <. y , z >. | ( ( A R y /\ B R y ) /\ ( A S z /\ B S z ) ) } )
9 8 neeq1d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) =/= (/) <-> { <. y , z >. | ( ( A R y /\ B R y ) /\ ( A S z /\ B S z ) ) } =/= (/) ) )
10 opabn0 
 |-  ( { <. y , z >. | ( ( A R y /\ B R y ) /\ ( A S z /\ B S z ) ) } =/= (/) <-> E. y E. z ( ( A R y /\ B R y ) /\ ( A S z /\ B S z ) ) )
11 9 10 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) =/= (/) <-> E. y E. z ( ( A R y /\ B R y ) /\ ( A S z /\ B S z ) ) ) )
12 exdistrv 
 |-  ( E. y E. z ( ( A R y /\ B R y ) /\ ( A S z /\ B S z ) ) <-> ( E. y ( A R y /\ B R y ) /\ E. z ( A S z /\ B S z ) ) )
13 11 12 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) =/= (/) <-> ( E. y ( A R y /\ B R y ) /\ E. z ( A S z /\ B S z ) ) ) )
14 ecinn0 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] R i^i [ B ] R ) =/= (/) <-> E. y ( A R y /\ B R y ) ) )
15 ecinn0 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] S i^i [ B ] S ) =/= (/) <-> E. z ( A S z /\ B S z ) ) )
16 14 15 anbi12d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( ( [ A ] R i^i [ B ] R ) =/= (/) /\ ( [ A ] S i^i [ B ] S ) =/= (/) ) <-> ( E. y ( A R y /\ B R y ) /\ E. z ( A S z /\ B S z ) ) ) )
17 13 16 bitr4d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) =/= (/) <-> ( ( [ A ] R i^i [ B ] R ) =/= (/) /\ ( [ A ] S i^i [ B ] S ) =/= (/) ) ) )
18 neanior 
 |-  ( ( ( [ A ] R i^i [ B ] R ) =/= (/) /\ ( [ A ] S i^i [ B ] S ) =/= (/) ) <-> -. ( ( [ A ] R i^i [ B ] R ) = (/) \/ ( [ A ] S i^i [ B ] S ) = (/) ) )
19 17 18 bitrdi 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) =/= (/) <-> -. ( ( [ A ] R i^i [ B ] R ) = (/) \/ ( [ A ] S i^i [ B ] S ) = (/) ) ) )
20 19 necon4abid 
 |-  ( ( A e. V /\ B e. W ) -> ( ( [ A ] ( R |X. S ) i^i [ B ] ( R |X. S ) ) = (/) <-> ( ( [ A ] R i^i [ B ] R ) = (/) \/ ( [ A ] S i^i [ B ] S ) = (/) ) ) )