Metamath Proof Explorer

Theorem disjdmqsss

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

Ref Expression
Assertion disjdmqsss ⊢DisjR→dom⁡R/R⊆dom⁡≀R/≀R

Proof

Step Hyp Ref Expression
1 disjrel ⊢DisjR→Rel⁡R
2 releldmqs ⊢v∈V→Rel⁡R→v∈dom⁡R/R↔∃u∈dom⁡R∃x∈uRv=uR
3 2 elv ⊢Rel⁡R→v∈dom⁡R/R↔∃u∈dom⁡R∃x∈uRv=uR
4 1 3 syl ⊢DisjR→v∈dom⁡R/R↔∃u∈dom⁡R∃x∈uRv=uR
5 disjlem19 ⊢x∈V→DisjR→u∈dom⁡R∧x∈uR→uR=x≀R
6 5 elv ⊢DisjR→u∈dom⁡R∧x∈uR→uR=x≀R
7 6 ralrimivv ⊢DisjR→∀u∈dom⁡R∀x∈uRuR=x≀R
8 2r19.29 ⊢∀u∈dom⁡R∀x∈uRuR=x≀R∧∃u∈dom⁡R∃x∈uRv=uR→∃u∈dom⁡R∃x∈uRuR=x≀R∧v=uR
9 8 ex ⊢∀u∈dom⁡R∀x∈uRuR=x≀R→∃u∈dom⁡R∃x∈uRv=uR→∃u∈dom⁡R∃x∈uRuR=x≀R∧v=uR
10 7 9 syl ⊢DisjR→∃u∈dom⁡R∃x∈uRv=uR→∃u∈dom⁡R∃x∈uRuR=x≀R∧v=uR
11 4 10 sylbid ⊢DisjR→v∈dom⁡R/R→∃u∈dom⁡R∃x∈uRuR=x≀R∧v=uR
12 eqtr ⊢v=uR∧uR=x≀R→v=x≀R
13 12 ancoms ⊢uR=x≀R∧v=uR→v=x≀R
14 13 reximi ⊢∃x∈uRuR=x≀R∧v=uR→∃x∈uRv=x≀R
15 14 reximi ⊢∃u∈dom⁡R∃x∈uRuR=x≀R∧v=uR→∃u∈dom⁡R∃x∈uRv=x≀R
16 11 15 syl6 ⊢DisjR→v∈dom⁡R/R→∃u∈dom⁡R∃x∈uRv=x≀R
17 releldmqscoss ⊢v∈V→Rel⁡R→v∈dom⁡≀R/≀R↔∃u∈dom⁡R∃x∈uRv=x≀R
18 17 elv ⊢Rel⁡R→v∈dom⁡≀R/≀R↔∃u∈dom⁡R∃x∈uRv=x≀R
19 1 18 syl ⊢DisjR→v∈dom⁡≀R/≀R↔∃u∈dom⁡R∃x∈uRv=x≀R
20 16 19 sylibrd ⊢DisjR→v∈dom⁡R/R→v∈dom⁡≀R/≀R
21 20 ssrdv ⊢DisjR→dom⁡R/R⊆dom⁡≀R/≀R