psref

		Ref	Expression
	Hypothesis	psref.1	$⊢ X = dom R$
	Assertion	psref	$⊢ (R \in PosetRel \land A \in X) \to A R A$

Step	Hyp	Ref	Expression
1		psref.1	$⊢ X = dom R$
2		psdmrn	$⊢ R \in PosetRel \to (dom R = ⋃ ⋃ R \land ran R = ⋃ ⋃ R)$
3	2	simpld	$⊢ R \in PosetRel \to dom R = ⋃ ⋃ R$
4	1 3	eqtrid	$⊢ R \in PosetRel \to X = ⋃ ⋃ R$
5	4	eleq2d	$⊢ R \in PosetRel \to (A \in X \leftrightarrow A \in ⋃ ⋃ R)$
6		pslem	$⊢ R \in PosetRel \to (((A R A \land A R A) \to A R A) \land (A \in ⋃ ⋃ R \to A R A) \land ((A R A \land A R A) \to A = A))$
7	6	simp2d	$⊢ R \in PosetRel \to (A \in ⋃ ⋃ R \to A R A)$
8	5 7	sylbid	$⊢ R \in PosetRel \to (A \in X \to A R A)$
9	8	imp	$⊢ (R \in PosetRel \land A \in X) \to A R A$

Metamath Proof Explorer