Metamath Proof Explorer

Theorem disjdmqscossss

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

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

Proof

Step Hyp Ref Expression
1 disjrel ⊢DisjR→Rel⁡R
2 releldmqscoss ⊢v∈V→Rel⁡R→v∈dom⁡≀R/≀R↔∃u∈dom⁡R∃x∈uRv=x≀R
3 2 elv ⊢Rel⁡R→v∈dom⁡≀R/≀R↔∃u∈dom⁡R∃x∈uRv=x≀R
4 1 3 syl ⊢DisjR→v∈dom⁡≀R/≀R↔∃u∈dom⁡R∃x∈uRv=x≀R
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=x≀R→∃u∈dom⁡R∃x∈uRuR=x≀R∧v=x≀R
9 8 ex ⊢∀u∈dom⁡R∀x∈uRuR=x≀R→∃u∈dom⁡R∃x∈uRv=x≀R→∃u∈dom⁡R∃x∈uRuR=x≀R∧v=x≀R
10 7 9 syl ⊢DisjR→∃u∈dom⁡R∃x∈uRv=x≀R→∃u∈dom⁡R∃x∈uRuR=x≀R∧v=x≀R
11 4 10 sylbid ⊢DisjR→v∈dom⁡≀R/≀R→∃u∈dom⁡R∃x∈uRuR=x≀R∧v=x≀R
12 eqtr3 ⊢uR=x≀R∧v=x≀R→uR=v
13 12 reximi ⊢∃x∈uRuR=x≀R∧v=x≀R→∃x∈uRuR=v
14 13 reximi ⊢∃u∈dom⁡R∃x∈uRuR=x≀R∧v=x≀R→∃u∈dom⁡R∃x∈uRuR=v
15 11 14 syl6 ⊢DisjR→v∈dom⁡≀R/≀R→∃u∈dom⁡R∃x∈uRuR=v
16 df-rex ⊢∃x∈uRuR=v↔∃xx∈uR∧uR=v
17 19.41v ⊢∃xx∈uR∧uR=v↔∃xx∈uR∧uR=v
18 16 17 bitri ⊢∃x∈uRuR=v↔∃xx∈uR∧uR=v
19 18 simprbi ⊢∃x∈uRuR=v→uR=v
20 19 reximi ⊢∃u∈dom⁡R∃x∈uRuR=v→∃u∈dom⁡RuR=v
21 15 20 syl6 ⊢DisjR→v∈dom⁡≀R/≀R→∃u∈dom⁡RuR=v
22 eqcom ⊢uR=v↔v=uR
23 22 rexbii ⊢∃u∈dom⁡RuR=v↔∃u∈dom⁡Rv=uR
24 21 23 imbitrdi ⊢DisjR→v∈dom⁡≀R/≀R→∃u∈dom⁡Rv=uR
25 24 ss2abdv ⊢DisjR→v|v∈dom⁡≀R/≀R⊆v|∃u∈dom⁡Rv=uR
26 abid1 ⊢dom⁡≀R/≀R=v|v∈dom⁡≀R/≀R
27 df-qs ⊢dom⁡R/R=v|∃u∈dom⁡Rv=uR
28 25 26 27 3sstr4g ⊢DisjR→dom⁡≀R/≀R⊆dom⁡R/R