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 e. PosetRel /\ A C_ X ) -> dom ( R i^i ( A X. A ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		psssdm.1	|- X = dom R
2	1	psssdm2	|- ( R e. PosetRel -> dom ( R i^i ( A X. A ) ) = ( X i^i A ) )
3		sseqin2	|- ( A C_ X <-> ( X i^i A ) = A )
4	3	biimpi	|- ( A C_ X -> ( X i^i A ) = A )
5	2 4	sylan9eq	|- ( ( R e. PosetRel /\ A C_ X ) -> dom ( R i^i ( A X. A ) ) = A )