disjdmqscossss

		Ref	Expression
	Assertion	disjdmqscossss	$⊢ Disj R \to dom ≀ R / ≀ R \subseteq dom R / R$

Proof

Step	Hyp	Ref	Expression
1		disjrel	$⊢ Disj R \to Rel R$
2		releldmqscoss	$⊢ v \in V \to (Rel R \to (v \in (dom ≀ R / ≀ R) \leftrightarrow \exists u \in dom R \exists x \in [u] R v = [x] ≀ R))$
3	2	elv	$⊢ Rel R \to (v \in (dom ≀ R / ≀ R) \leftrightarrow \exists u \in dom R \exists x \in [u] R v = [x] ≀ R)$
4	1 3	syl	$⊢ Disj R \to (v \in (dom ≀ R / ≀ R) \leftrightarrow \exists u \in dom R \exists x \in [u] R v = [x] ≀ R)$
5		disjlem19	$⊢ x \in V \to (Disj R \to ((u \in dom R \land x \in [u] R) \to [u] R = [x] ≀ R))$
6	5	elv	$⊢ Disj R \to ((u \in dom R \land x \in [u] R) \to [u] R = [x] ≀ R)$
7	6	ralrimivv	$⊢ Disj R \to \forall u \in dom R \forall x \in [u] R [u] R = [x] ≀ R$
8		2r19.29	$⊢ (\forall u \in dom R \forall x \in [u] R [u] R = [x] ≀ R \land \exists u \in dom R \exists x \in [u] R v = [x] ≀ R) \to \exists u \in dom R \exists x \in [u] R ([u] R = [x] ≀ R \land v = [x] ≀ R)$
9	8	ex	$⊢ \forall u \in dom R \forall x \in [u] R [u] R = [x] ≀ R \to (\exists u \in dom R \exists x \in [u] R v = [x] ≀ R \to \exists u \in dom R \exists x \in [u] R ([u] R = [x] ≀ R \land v = [x] ≀ R))$
10	7 9	syl	$⊢ Disj R \to (\exists u \in dom R \exists x \in [u] R v = [x] ≀ R \to \exists u \in dom R \exists x \in [u] R ([u] R = [x] ≀ R \land v = [x] ≀ R))$
11	4 10	sylbid	$⊢ Disj R \to (v \in (dom ≀ R / ≀ R) \to \exists u \in dom R \exists x \in [u] R ([u] R = [x] ≀ R \land v = [x] ≀ R))$
12		eqtr3	$⊢ ([u] R = [x] ≀ R \land v = [x] ≀ R) \to [u] R = v$
13	12	reximi	$⊢ \exists x \in [u] R ([u] R = [x] ≀ R \land v = [x] ≀ R) \to \exists x \in [u] R [u] R = v$
14	13	reximi	$⊢ \exists u \in dom R \exists x \in [u] R ([u] R = [x] ≀ R \land v = [x] ≀ R) \to \exists u \in dom R \exists x \in [u] R [u] R = v$
15	11 14	syl6	$⊢ Disj R \to (v \in (dom ≀ R / ≀ R) \to \exists u \in dom R \exists x \in [u] R [u] R = v)$
16		df-rex	$⊢ \exists x \in [u] R [u] R = v \leftrightarrow \exists x (x \in [u] R \land [u] R = v)$
17		19.41v	$⊢ \exists x (x \in [u] R \land [u] R = v) \leftrightarrow (\exists x x \in [u] R \land [u] R = v)$
18	16 17	bitri	$⊢ \exists x \in [u] R [u] R = v \leftrightarrow (\exists x x \in [u] R \land [u] R = v)$
19	18	simprbi	$⊢ \exists x \in [u] R [u] R = v \to [u] R = v$
20	19	reximi	$⊢ \exists u \in dom R \exists x \in [u] R [u] R = v \to \exists u \in dom R [u] R = v$
21	15 20	syl6	$⊢ Disj R \to (v \in (dom ≀ R / ≀ R) \to \exists u \in dom R [u] R = v)$
22		eqcom	$⊢ [u] R = v \leftrightarrow v = [u] R$
23	22	rexbii	$⊢ \exists u \in dom R [u] R = v \leftrightarrow \exists u \in dom R v = [u] R$
24	21 23	imbitrdi	$⊢ Disj R \to (v \in (dom ≀ R / ≀ R) \to \exists u \in dom R v = [u] R)$
25	24	ss2abdv	$⊢ Disj R \to \{v \| v \in (dom ≀ R / ≀ R)\} \subseteq \{v \| \exists u \in dom R v = [u] R\}$
26		abid1	$⊢ dom ≀ R / ≀ R = \{v \| v \in (dom ≀ R / ≀ R)\}$
27		df-qs	$⊢ dom R / R = \{v \| \exists u \in dom R v = [u] R\}$
28	25 26 27	3sstr4g	$⊢ Disj R \to dom ≀ R / ≀ R \subseteq dom R / R$

Metamath Proof Explorer

Theorem disjdmqscossss

Proof