refressn

Description: Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 ) is reflexive, see also refrelressn . (Contributed by Peter Mazsa, 12-Jun-2024)

		Ref	Expression
	Assertion	refressn	$⊢ A \in V \to \forall x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) x ({R ↾}_{\{A\}}) x$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) \leftrightarrow (x \in dom ({R ↾}_{\{A\}}) \land x \in ran ({R ↾}_{\{A\}}))$
2		eldmressnALTV	$⊢ x \in V \to (x \in dom ({R ↾}_{\{A\}}) \leftrightarrow (x = A \land A \in dom R))$
3	2	elv	$⊢ x \in dom ({R ↾}_{\{A\}}) \leftrightarrow (x = A \land A \in dom R)$
4	3	simplbi	$⊢ x \in dom ({R ↾}_{\{A\}}) \to x = A$
5	4	adantr	$⊢ (x \in dom ({R ↾}_{\{A\}}) \land x \in ran ({R ↾}_{\{A\}})) \to x = A$
6	1 5	sylbi	$⊢ x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) \to x = A$
7	6	a1i	$⊢ A \in V \to (x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) \to x = A)$
8		elrnressn	$⊢ (A \in V \land x \in V) \to (x \in ran ({R ↾}_{\{A\}}) \leftrightarrow A R x)$
9	8	elvd	$⊢ A \in V \to (x \in ran ({R ↾}_{\{A\}}) \leftrightarrow A R x)$
10	9	biimpd	$⊢ A \in V \to (x \in ran ({R ↾}_{\{A\}}) \to A R x)$
11	10	adantld	$⊢ A \in V \to ((x \in dom ({R ↾}_{\{A\}}) \land x \in ran ({R ↾}_{\{A\}})) \to A R x)$
12	1 11	biimtrid	$⊢ A \in V \to (x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) \to A R x)$
13	4	eqcomd	$⊢ x \in dom ({R ↾}_{\{A\}}) \to A = x$
14	13	breq1d	$⊢ x \in dom ({R ↾}_{\{A\}}) \to (A R x \leftrightarrow x R x)$
15	14	adantr	$⊢ (x \in dom ({R ↾}_{\{A\}}) \land x \in ran ({R ↾}_{\{A\}})) \to (A R x \leftrightarrow x R x)$
16	1 15	sylbi	$⊢ x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) \to (A R x \leftrightarrow x R x)$
17	12 16	mpbidi	$⊢ A \in V \to (x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) \to x R x)$
18	7 17	jcad	$⊢ A \in V \to (x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) \to (x = A \land x R x))$
19		brressn	$⊢ (x \in V \land x \in V) \to (x ({R ↾}_{\{A\}}) x \leftrightarrow (x = A \land x R x))$
20	19	el2v	$⊢ x ({R ↾}_{\{A\}}) x \leftrightarrow (x = A \land x R x)$
21	18 20	imbitrrdi	$⊢ A \in V \to (x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) \to x ({R ↾}_{\{A\}}) x)$
22	21	ralrimiv	$⊢ A \in V \to \forall x \in (dom ({R ↾}_{\{A\}}) \cap ran ({R ↾}_{\{A\}})) x ({R ↾}_{\{A\}}) x$

Metamath Proof Explorer

Theorem refressn

Proof