Metamath Proof Explorer

Theorem psssdm2

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

Ref Expression
Hypothesis psssdm.1 
|- X = dom R
Assertion psssdm2 
|- ( R e. PosetRel -> dom ( R i^i ( A X. A ) ) = ( X i^i A ) )

Proof

Step Hyp Ref Expression
1 psssdm.1 
 |-  X = dom R
2 dmin 
 |-  dom ( R i^i ( A X. A ) ) C_ ( dom R i^i dom ( A X. A ) )
3 1 eqcomi 
 |-  dom R = X
4 dmxpid 
 |-  dom ( A X. A ) = A
5 3 4 ineq12i 
 |-  ( dom R i^i dom ( A X. A ) ) = ( X i^i A )
6 2 5 sseqtri 
 |-  dom ( R i^i ( A X. A ) ) C_ ( X i^i A )
7 6 a1i 
 |-  ( R e. PosetRel -> dom ( R i^i ( A X. A ) ) C_ ( X i^i A ) )
8 simpr 
 |-  ( ( R e. PosetRel /\ x e. ( X i^i A ) ) -> x e. ( X i^i A ) )
9 8 elin2d 
 |-  ( ( R e. PosetRel /\ x e. ( X i^i A ) ) -> x e. A )
10 elinel1 
 |-  ( x e. ( X i^i A ) -> x e. X )
11 1 psref 
 |-  ( ( R e. PosetRel /\ x e. X ) -> x R x )
12 10 11 sylan2 
 |-  ( ( R e. PosetRel /\ x e. ( X i^i A ) ) -> x R x )
13 brinxp2 
 |-  ( x ( R i^i ( A X. A ) ) x <-> ( ( x e. A /\ x e. A ) /\ x R x ) )
14 9 9 12 13 syl21anbrc 
 |-  ( ( R e. PosetRel /\ x e. ( X i^i A ) ) -> x ( R i^i ( A X. A ) ) x )
15 vex 
 |-  x e. _V
16 15 15 breldm 
 |-  ( x ( R i^i ( A X. A ) ) x -> x e. dom ( R i^i ( A X. A ) ) )
17 14 16 syl 
 |-  ( ( R e. PosetRel /\ x e. ( X i^i A ) ) -> x e. dom ( R i^i ( A X. A ) ) )
18 7 17 eqelssd 
 |-  ( R e. PosetRel -> dom ( R i^i ( A X. A ) ) = ( X i^i A ) )