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 ⊆ dom ⁡ ≀ R / ≀ R

Proof

Step Hyp Ref Expression
1 disjrel ⊢ Disj R → Rel ⁡ R
2 releldmqs ⊢ v ∈ V → Rel ⁡ R → v ∈ dom ⁡ R / R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = u R
3 2 elv ⊢ Rel ⁡ R → v ∈ dom ⁡ R / R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = u R
4 1 3 syl ⊢ Disj R → v ∈ dom ⁡ R / R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = u R
5 disjlem19 ⊢ x ∈ V → Disj R → u ∈ dom ⁡ R ∧ x ∈ u R → u R = x ≀ R
6 5 elv ⊢ Disj R → u ∈ dom ⁡ R ∧ x ∈ u R → u R = x ≀ R
7 6 ralrimivv ⊢ Disj R → ∀ u ∈ dom ⁡ R ∀ x ∈ u R u R = x ≀ R
8 2r19.29 ⊢ ∀ u ∈ dom ⁡ R ∀ x ∈ u R u R = x ≀ R ∧ ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = u R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R u R = x ≀ R ∧ v = u R
9 8 ex ⊢ ∀ u ∈ dom ⁡ R ∀ x ∈ u R u R = x ≀ R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = u R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R u R = x ≀ R ∧ v = u R
10 7 9 syl ⊢ Disj R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = u R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R u R = x ≀ R ∧ v = u R
11 4 10 sylbid ⊢ Disj R → v ∈ dom ⁡ R / R → ∃ u ∈ dom ⁡ R ∃ x ∈ 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 ⊢ ∃ x ∈ u R u R = x ≀ R ∧ v = u R → ∃ x ∈ u R v = x ≀ R
15 14 reximi ⊢ ∃ u ∈ dom ⁡ R ∃ x ∈ u R u R = x ≀ R ∧ v = u R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = x ≀ R
16 11 15 syl6 ⊢ Disj R → v ∈ dom ⁡ R / R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = x ≀ R
17 releldmqscoss ⊢ v ∈ V → Rel ⁡ R → v ∈ dom ⁡ ≀ R / ≀ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = x ≀ R
18 17 elv ⊢ Rel ⁡ R → v ∈ dom ⁡ ≀ R / ≀ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = x ≀ R
19 1 18 syl ⊢ Disj R → v ∈ dom ⁡ ≀ R / ≀ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R v = x ≀ R
20 16 19 sylibrd ⊢ Disj R → v ∈ dom ⁡ R / R → v ∈ dom ⁡ ≀ R / ≀ R
21 20 ssrdv ⊢ Disj R → dom ⁡ R / R ⊆ dom ⁡ ≀ R / ≀ R