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	⊢ 𝑋 = dom 𝑅
Assertion	psssdm	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		psssdm.1	⊢ 𝑋 = dom 𝑅
2	1	psssdm2	⊢ ( 𝑅 ∈ PosetRel → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( 𝑋 ∩ 𝐴 ) )
3		sseqin2	⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝐴 ) = 𝐴 )
4	3	biimpi	⊢ ( 𝐴 ⊆ 𝑋 → ( 𝑋 ∩ 𝐴 ) = 𝐴 )
5	2 4	sylan9eq	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )