Metamath Proof Explorer

Theorem disjlem17

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

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

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( E. y e. dom R ( A e. [ y ] R /\ B e. [ y ] R ) <-> E. y ( y e. dom R /\ ( A e. [ y ] R /\ B e. [ y ] R ) ) )
2 an32 
 |-  ( ( ( x e. dom R /\ y e. dom R ) /\ A e. [ x ] R ) <-> ( ( x e. dom R /\ A e. [ x ] R ) /\ y e. dom R ) )
3 disjlem14 
 |-  ( Disj R -> ( ( x e. dom R /\ y e. dom R ) -> ( ( A e. [ x ] R /\ A e. [ y ] R ) -> [ x ] R = [ y ] R ) ) )
4 eleq2 
 |-  ( [ x ] R = [ y ] R -> ( B e. [ x ] R <-> B e. [ y ] R ) )
5 4 biimprd 
 |-  ( [ x ] R = [ y ] R -> ( B e. [ y ] R -> B e. [ x ] R ) )
6 3 5 syl8 
 |-  ( Disj R -> ( ( x e. dom R /\ y e. dom R ) -> ( ( A e. [ x ] R /\ A e. [ y ] R ) -> ( B e. [ y ] R -> B e. [ x ] R ) ) ) )
7 6 exp4a 
 |-  ( Disj R -> ( ( x e. dom R /\ y e. dom R ) -> ( A e. [ x ] R -> ( A e. [ y ] R -> ( B e. [ y ] R -> B e. [ x ] R ) ) ) ) )
8 7 impd 
 |-  ( Disj R -> ( ( ( x e. dom R /\ y e. dom R ) /\ A e. [ x ] R ) -> ( A e. [ y ] R -> ( B e. [ y ] R -> B e. [ x ] R ) ) ) )
9 2 8 biimtrrid 
 |-  ( Disj R -> ( ( ( x e. dom R /\ A e. [ x ] R ) /\ y e. dom R ) -> ( A e. [ y ] R -> ( B e. [ y ] R -> B e. [ x ] R ) ) ) )
10 9 expd 
 |-  ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( y e. dom R -> ( A e. [ y ] R -> ( B e. [ y ] R -> B e. [ x ] R ) ) ) ) )
11 10 imp5a 
 |-  ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( y e. dom R -> ( ( A e. [ y ] R /\ B e. [ y ] R ) -> B e. [ x ] R ) ) ) )
12 11 imp4b 
 |-  ( ( Disj R /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( ( y e. dom R /\ ( A e. [ y ] R /\ B e. [ y ] R ) ) -> B e. [ x ] R ) )
13 12 exlimdv 
 |-  ( ( Disj R /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( E. y ( y e. dom R /\ ( A e. [ y ] R /\ B e. [ y ] R ) ) -> B e. [ x ] R ) )
14 1 13 biimtrid 
 |-  ( ( Disj R /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( E. y e. dom R ( A e. [ y ] R /\ B e. [ y ] R ) -> B e. [ x ] R ) )
15 14 ex 
 |-  ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( E. y e. dom R ( A e. [ y ] R /\ B e. [ y ] R ) -> B e. [ x ] R ) ) )