This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psssdm

Description: Field of a subposet. (Contributed by FL, 19-Sep-2011) (Revised by Mario Carneiro, 9-Sep-2015)

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

Step	Hyp	Ref	Expression
1		psssdm.1	$⊢ X = dom R$
2	1	psssdm2	$⊢ R \in PosetRel \to dom (R \cap (A \times A)) = X \cap A$
3		sseqin2	$⊢ A \subseteq X \leftrightarrow X \cap A = A$
4	3	biimpi	$⊢ A \subseteq X \to X \cap A = A$
5	2 4	sylan9eq	$⊢ (R \in PosetRel \land A \subseteq X) \to dom (R \cap (A \times A)) = A$