prsrn

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

	Ref	Expression
Hypotheses	ordtNEW.b	$⊢ B = {Base}_{K}$
	ordtNEW.l	$⊢ \underset{˙}{\leq} = \leq_{K} \cap (B \times B)$
Assertion	prsrn	$⊢ K \in Proset \to ran \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	rneqi	$⊢ ran \underset{˙}{\leq} = ran (\leq_{K} \cap (B \times B))$
4	3	eleq2i	$⊢ x \in ran \underset{˙}{\leq} \leftrightarrow x \in ran (\leq_{K} \cap (B \times B))$
5		vex	$⊢ x \in V$
6	5	elrn2	$⊢ x \in ran (\leq_{K} \cap (B \times B)) \leftrightarrow \exists y ⟨y, x⟩ \in (\leq_{K} \cap (B \times B))$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8	1 7	prsref	$⊢ (K \in Proset \land x \in B) \to x \leq_{K} x$
9		df-br	$⊢ x \leq_{K} x \leftrightarrow ⟨x, x⟩ \in \leq_{K}$
10	8 9	sylib	$⊢ (K \in Proset \land x \in B) \to ⟨x, x⟩ \in \leq_{K}$
11		simpr	$⊢ (K \in Proset \land x \in B) \to x \in B$
12	11 11	opelxpd	$⊢ (K \in Proset \land x \in B) \to ⟨x, x⟩ \in (B \times B)$
13	10 12	elind	$⊢ (K \in Proset \land x \in B) \to ⟨x, x⟩ \in (\leq_{K} \cap (B \times B))$
14		opeq1	$⊢ y = x \to ⟨y, x⟩ = ⟨x, x⟩$
15	14	eleq1d	$⊢ y = x \to (⟨y, x⟩ \in (\leq_{K} \cap (B \times B)) \leftrightarrow ⟨x, x⟩ \in (\leq_{K} \cap (B \times B)))$
16	5 15	spcev	$⊢ ⟨x, x⟩ \in (\leq_{K} \cap (B \times B)) \to \exists y ⟨y, x⟩ \in (\leq_{K} \cap (B \times B))$
17	13 16	syl	$⊢ (K \in Proset \land x \in B) \to \exists y ⟨y, x⟩ \in (\leq_{K} \cap (B \times B))$
18	17	ex	$⊢ K \in Proset \to (x \in B \to \exists y ⟨y, x⟩ \in (\leq_{K} \cap (B \times B)))$
19		elinel2	$⊢ ⟨y, x⟩ \in (\leq_{K} \cap (B \times B)) \to ⟨y, x⟩ \in (B \times B)$
20		opelxp2	$⊢ ⟨y, x⟩ \in (B \times B) \to x \in B$
21	19 20	syl	$⊢ ⟨y, x⟩ \in (\leq_{K} \cap (B \times B)) \to x \in B$
22	21	exlimiv	$⊢ \exists y ⟨y, x⟩ \in (\leq_{K} \cap (B \times B)) \to x \in B$
23	18 22	impbid1	$⊢ K \in Proset \to (x \in B \leftrightarrow \exists y ⟨y, x⟩ \in (\leq_{K} \cap (B \times B)))$
24	6 23	bitr4id	$⊢ K \in Proset \to (x \in ran (\leq_{K} \cap (B \times B)) \leftrightarrow x \in B)$
25	4 24	bitrid	$⊢ K \in Proset \to (x \in ran \underset{˙}{\leq} \leftrightarrow x \in B)$
26	25	eqrdv	$⊢ K \in Proset \to ran \underset{˙}{\leq} = B$

Metamath Proof Explorer

Theorem prsrn

Proof