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

Metamath Proof Explorer

Theorem disjlem18

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

Ref Expression
Assertion disjlem18 
|- ( ( A e. V /\ B e. W ) -> ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( B e. [ x ] R <-> A ,~ R B ) ) ) )

Proof

Step Hyp Ref Expression
1 rspe 
 |-  ( ( x e. dom R /\ ( A e. [ x ] R /\ B e. [ x ] R ) ) -> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) )
2 1 expr 
 |-  ( ( x e. dom R /\ A e. [ x ] R ) -> ( B e. [ x ] R -> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) )
3 2 adantl 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ Disj R ) /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( B e. [ x ] R -> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) )
4 relbrcoss 
 |-  ( ( A e. V /\ B e. W ) -> ( Rel R -> ( A ,~ R B <-> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) ) )
5 disjrel 
 |-  ( Disj R -> Rel R )
6 4 5 impel 
 |-  ( ( ( A e. V /\ B e. W ) /\ Disj R ) -> ( A ,~ R B <-> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) )
7 6 adantr 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ Disj R ) /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( A ,~ R B <-> E. x e. dom R ( A e. [ x ] R /\ B e. [ x ] R ) ) )
8 3 7 sylibrd 
 |-  ( ( ( ( A e. V /\ B e. W ) /\ Disj R ) /\ ( x e. dom R /\ A e. [ x ] R ) ) -> ( B e. [ x ] R -> A ,~ R B ) )
9 8 ex 
 |-  ( ( ( A e. V /\ B e. W ) /\ Disj R ) -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( B e. [ x ] R -> A ,~ R B ) ) )
10 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 ) ) )
11 10 adantl 
 |-  ( ( ( A e. V /\ B e. W ) /\ 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 ) ) )
12 relbrcoss 
 |-  ( ( A e. V /\ B e. W ) -> ( Rel R -> ( A ,~ R B <-> E. y e. dom R ( A e. [ y ] R /\ B e. [ y ] R ) ) ) )
13 12 5 impel 
 |-  ( ( ( A e. V /\ B e. W ) /\ Disj R ) -> ( A ,~ R B <-> E. y e. dom R ( A e. [ y ] R /\ B e. [ y ] R ) ) )
14 13 imbi1d 
 |-  ( ( ( A e. V /\ B e. W ) /\ Disj R ) -> ( ( A ,~ R B -> B e. [ x ] R ) <-> ( E. y e. dom R ( A e. [ y ] R /\ B e. [ y ] R ) -> B e. [ x ] R ) ) )
15 11 14 sylibrd 
 |-  ( ( ( A e. V /\ B e. W ) /\ Disj R ) -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( A ,~ R B -> B e. [ x ] R ) ) )
16 9 15 impbidd 
 |-  ( ( ( A e. V /\ B e. W ) /\ Disj R ) -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( B e. [ x ] R <-> A ,~ R B ) ) )
17 16 ex 
 |-  ( ( A e. V /\ B e. W ) -> ( Disj R -> ( ( x e. dom R /\ A e. [ x ] R ) -> ( B e. [ x ] R <-> A ,~ R B ) ) ) )