Metamath Proof Explorer

Theorem disjdmqsss

Description: Lemma for disjdmqseq via disjdmqs . (Contributed by Peter Mazsa, 16-Sep-2021)

Ref Expression
Assertion disjdmqsss 
|- ( Disj R -> ( dom R /. R ) C_ ( dom ,~ R /. ,~ R ) )

Proof

Step Hyp Ref Expression
1 disjrel 
 |-  ( Disj R -> Rel R )
2 releldmqs 
 |-  ( v e. _V -> ( Rel R -> ( v e. ( dom R /. R ) <-> E. u e. dom R E. x e. [ u ] R v = [ u ] R ) ) )
3 2 elv 
 |-  ( Rel R -> ( v e. ( dom R /. R ) <-> E. u e. dom R E. x e. [ u ] R v = [ u ] R ) )
4 1 3 syl 
 |-  ( Disj R -> ( v e. ( dom R /. R ) <-> E. u e. dom R E. x e. [ u ] R v = [ u ] R ) )
5 disjlem19 
 |-  ( x e. _V -> ( Disj R -> ( ( u e. dom R /\ x e. [ u ] R ) -> [ u ] R = [ x ] ,~ R ) ) )
6 5 elv 
 |-  ( Disj R -> ( ( u e. dom R /\ x e. [ u ] R ) -> [ u ] R = [ x ] ,~ R ) )
7 6 ralrimivv 
 |-  ( Disj R -> A. u e. dom R A. x e. [ u ] R [ u ] R = [ x ] ,~ R )
8 2r19.29 
 |-  ( ( A. u e. dom R A. x e. [ u ] R [ u ] R = [ x ] ,~ R /\ E. u e. dom R E. x e. [ u ] R v = [ u ] R ) -> E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ u ] R ) )
9 8 ex 
 |-  ( A. u e. dom R A. x e. [ u ] R [ u ] R = [ x ] ,~ R -> ( E. u e. dom R E. x e. [ u ] R v = [ u ] R -> E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ u ] R ) ) )
10 7 9 syl 
 |-  ( Disj R -> ( E. u e. dom R E. x e. [ u ] R v = [ u ] R -> E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ u ] R ) ) )
11 4 10 sylbid 
 |-  ( Disj R -> ( v e. ( dom R /. R ) -> E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ u ] R ) ) )
12 eqtr 
 |-  ( ( v = [ u ] R /\ [ u ] R = [ x ] ,~ R ) -> v = [ x ] ,~ R )
13 12 ancoms 
 |-  ( ( [ u ] R = [ x ] ,~ R /\ v = [ u ] R ) -> v = [ x ] ,~ R )
14 13 reximi 
 |-  ( E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ u ] R ) -> E. x e. [ u ] R v = [ x ] ,~ R )
15 14 reximi 
 |-  ( E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ u ] R ) -> E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ R )
16 11 15 syl6 
 |-  ( Disj R -> ( v e. ( dom R /. R ) -> E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ R ) )
17 releldmqscoss 
 |-  ( v e. _V -> ( Rel R -> ( v e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ R ) ) )
18 17 elv 
 |-  ( Rel R -> ( v e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ R ) )
19 1 18 syl 
 |-  ( Disj R -> ( v e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ R ) )
20 16 19 sylibrd 
 |-  ( Disj R -> ( v e. ( dom R /. R ) -> v e. ( dom ,~ R /. ,~ R ) ) )
21 20 ssrdv 
 |-  ( Disj R -> ( dom R /. R ) C_ ( dom ,~ R /. ,~ R ) )