prsdm

Description: Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015)

	Ref	Expression
Hypotheses	ordtNEW.b	$⊢ B = {Base}_{K}$
	ordtNEW.l	$⊢ \underset{˙}{\leq} = \leq_{K} \cap (B \times B)$
Assertion	prsdm	$⊢ K \in Proset \to dom \underset{˙}{\leq} = B$

Proof

Step	Hyp	Ref	Expression
1		ordtNEW.b	$⊢ B = {Base}_{K}$
2		ordtNEW.l	$⊢ \underset{˙}{\leq} = \leq_{K} \cap (B \times B)$
3	2	dmeqi	$⊢ dom \underset{˙}{\leq} = dom (\leq_{K} \cap (B \times B))$
4	3	eleq2i	$⊢ x \in dom \underset{˙}{\leq} \leftrightarrow x \in dom (\leq_{K} \cap (B \times B))$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6	1 5	prsref	$⊢ (K \in Proset \land x \in B) \to x \leq_{K} x$
7		df-br	$⊢ x \leq_{K} x \leftrightarrow ⟨x, x⟩ \in \leq_{K}$
8	6 7	sylib	$⊢ (K \in Proset \land x \in B) \to ⟨x, x⟩ \in \leq_{K}$
9		simpr	$⊢ (K \in Proset \land x \in B) \to x \in B$
10	9 9	opelxpd	$⊢ (K \in Proset \land x \in B) \to ⟨x, x⟩ \in (B \times B)$
11	8 10	elind	$⊢ (K \in Proset \land x \in B) \to ⟨x, x⟩ \in (\leq_{K} \cap (B \times B))$
12		vex	$⊢ x \in V$
13		opeq2	$⊢ y = x \to ⟨x, y⟩ = ⟨x, x⟩$
14	13	eleq1d	$⊢ y = x \to (⟨x, y⟩ \in (\leq_{K} \cap (B \times B)) \leftrightarrow ⟨x, x⟩ \in (\leq_{K} \cap (B \times B)))$
15	12 14	spcev	$⊢ ⟨x, x⟩ \in (\leq_{K} \cap (B \times B)) \to \exists y ⟨x, y⟩ \in (\leq_{K} \cap (B \times B))$
16	11 15	syl	$⊢ (K \in Proset \land x \in B) \to \exists y ⟨x, y⟩ \in (\leq_{K} \cap (B \times B))$
17	16	ex	$⊢ K \in Proset \to (x \in B \to \exists y ⟨x, y⟩ \in (\leq_{K} \cap (B \times B)))$
18		elinel2	$⊢ ⟨x, y⟩ \in (\leq_{K} \cap (B \times B)) \to ⟨x, y⟩ \in (B \times B)$
19		opelxp1	$⊢ ⟨x, y⟩ \in (B \times B) \to x \in B$
20	18 19	syl	$⊢ ⟨x, y⟩ \in (\leq_{K} \cap (B \times B)) \to x \in B$
21	20	exlimiv	$⊢ \exists y ⟨x, y⟩ \in (\leq_{K} \cap (B \times B)) \to x \in B$
22	17 21	impbid1	$⊢ K \in Proset \to (x \in B \leftrightarrow \exists y ⟨x, y⟩ \in (\leq_{K} \cap (B \times B)))$
23	12	eldm2	$⊢ x \in dom (\leq_{K} \cap (B \times B)) \leftrightarrow \exists y ⟨x, y⟩ \in (\leq_{K} \cap (B \times B))$
24	22 23	syl6rbbr	$⊢ K \in Proset \to (x \in dom (\leq_{K} \cap (B \times B)) \leftrightarrow x \in B)$
25	4 24	syl5bb	$⊢ K \in Proset \to (x \in dom \underset{˙}{\leq} \leftrightarrow x \in B)$
26	25	eqrdv	$⊢ K \in Proset \to dom \underset{˙}{\leq} = B$

Metamath Proof Explorer

Theorem prsdm

Proof