Metamath Proof Explorer

Theorem disjdmqscossss

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

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

Proof

Step Hyp Ref Expression
1 disjrel 
 |-  ( Disj R -> Rel R )
2 releldmqscoss 
 |-  ( v e. _V -> ( Rel R -> ( v e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ R ) ) )
3 2 elv 
 |-  ( Rel R -> ( v e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ R ) )
4 1 3 syl 
 |-  ( Disj R -> ( v e. ( dom ,~ R /. ,~ R ) <-> E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ 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 = [ x ] ,~ R ) -> E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ x ] ,~ 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 = [ x ] ,~ R -> E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ x ] ,~ R ) ) )
10 7 9 syl 
 |-  ( Disj R -> ( E. u e. dom R E. x e. [ u ] R v = [ x ] ,~ R -> E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ x ] ,~ 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 = [ x ] ,~ R ) ) )
12 eqtr3 
 |-  ( ( [ u ] R = [ x ] ,~ R /\ v = [ x ] ,~ R ) -> [ u ] R = v )
13 12 reximi 
 |-  ( E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ x ] ,~ R ) -> E. x e. [ u ] R [ u ] R = v )
14 13 reximi 
 |-  ( E. u e. dom R E. x e. [ u ] R ( [ u ] R = [ x ] ,~ R /\ v = [ x ] ,~ R ) -> E. u e. dom R E. x e. [ u ] R [ u ] R = v )
15 11 14 syl6 
 |-  ( Disj R -> ( v e. ( dom ,~ R /. ,~ R ) -> E. u e. dom R E. x e. [ u ] R [ u ] R = v ) )
16 df-rex 
 |-  ( E. x e. [ u ] R [ u ] R = v <-> E. x ( x e. [ u ] R /\ [ u ] R = v ) )
17 19.41v 
 |-  ( E. x ( x e. [ u ] R /\ [ u ] R = v ) <-> ( E. x x e. [ u ] R /\ [ u ] R = v ) )
18 16 17 bitri 
 |-  ( E. x e. [ u ] R [ u ] R = v <-> ( E. x x e. [ u ] R /\ [ u ] R = v ) )
19 18 simprbi 
 |-  ( E. x e. [ u ] R [ u ] R = v -> [ u ] R = v )
20 19 reximi 
 |-  ( E. u e. dom R E. x e. [ u ] R [ u ] R = v -> E. u e. dom R [ u ] R = v )
21 15 20 syl6 
 |-  ( Disj R -> ( v e. ( dom ,~ R /. ,~ R ) -> E. u e. dom R [ u ] R = v ) )
22 eqcom 
 |-  ( [ u ] R = v <-> v = [ u ] R )
23 22 rexbii 
 |-  ( E. u e. dom R [ u ] R = v <-> E. u e. dom R v = [ u ] R )
24 21 23 imbitrdi 
 |-  ( Disj R -> ( v e. ( dom ,~ R /. ,~ R ) -> E. u e. dom R v = [ u ] R ) )
25 24 ss2abdv 
 |-  ( Disj R -> { v | v e. ( dom ,~ R /. ,~ R ) } C_ { v | E. u e. dom R v = [ u ] R } )
26 abid1 
 |-  ( dom ,~ R /. ,~ R ) = { v | v e. ( dom ,~ R /. ,~ R ) }
27 df-qs 
 |-  ( dom R /. R ) = { v | E. u e. dom R v = [ u ] R }
28 25 26 27 3sstr4g 
 |-  ( Disj R -> ( dom ,~ R /. ,~ R ) C_ ( dom R /. R ) )