Metamath Proof Explorer

Theorem disjlem14

Description: Lemma for disjdmqseq , partim2 and petlem via disjlem17 , (general version of the former prtlem14 ). (Contributed by Peter Mazsa, 10-Sep-2021)

Ref Expression
Assertion disjlem14 
|- ( Disj R -> ( ( x e. dom R /\ y e. dom R ) -> ( ( A e. [ x ] R /\ A e. [ y ] R ) -> [ x ] R = [ y ] R ) ) )

Proof

Step Hyp Ref Expression
1 dfdisjALTV5 
 |-  ( Disj R <-> ( A. x e. dom R A. y e. dom R ( x = y \/ ( [ x ] R i^i [ y ] R ) = (/) ) /\ Rel R ) )
2 1 simplbi 
 |-  ( Disj R -> A. x e. dom R A. y e. dom R ( x = y \/ ( [ x ] R i^i [ y ] R ) = (/) ) )
3 rsp2 
 |-  ( A. x e. dom R A. y e. dom R ( x = y \/ ( [ x ] R i^i [ y ] R ) = (/) ) -> ( ( x e. dom R /\ y e. dom R ) -> ( x = y \/ ( [ x ] R i^i [ y ] R ) = (/) ) ) )
4 2 3 syl 
 |-  ( Disj R -> ( ( x e. dom R /\ y e. dom R ) -> ( x = y \/ ( [ x ] R i^i [ y ] R ) = (/) ) ) )
5 eceq1 
 |-  ( x = y -> [ x ] R = [ y ] R )
6 5 a1d 
 |-  ( x = y -> ( ( A e. [ x ] R /\ A e. [ y ] R ) -> [ x ] R = [ y ] R ) )
7 elin 
 |-  ( A e. ( [ x ] R i^i [ y ] R ) <-> ( A e. [ x ] R /\ A e. [ y ] R ) )
8 nel02 
 |-  ( ( [ x ] R i^i [ y ] R ) = (/) -> -. A e. ( [ x ] R i^i [ y ] R ) )
9 8 pm2.21d 
 |-  ( ( [ x ] R i^i [ y ] R ) = (/) -> ( A e. ( [ x ] R i^i [ y ] R ) -> [ x ] R = [ y ] R ) )
10 7 9 biimtrrid 
 |-  ( ( [ x ] R i^i [ y ] R ) = (/) -> ( ( A e. [ x ] R /\ A e. [ y ] R ) -> [ x ] R = [ y ] R ) )
11 6 10 jaoi 
 |-  ( ( x = y \/ ( [ x ] R i^i [ y ] R ) = (/) ) -> ( ( A e. [ x ] R /\ A e. [ y ] R ) -> [ x ] R = [ y ] R ) )
12 4 11 syl6 
 |-  ( Disj R -> ( ( x e. dom R /\ y e. dom R ) -> ( ( A e. [ x ] R /\ A e. [ y ] R ) -> [ x ] R = [ y ] R ) ) )