# 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 ∈ PosetRel → dom ⁡ R ∩ A × A = X ∩ A$

### Proof

Step Hyp Ref Expression
1 psssdm.1 $⊢ X = dom ⁡ R$
2 dmin $⊢ dom ⁡ R ∩ A × A ⊆ dom ⁡ R ∩ dom ⁡ A × A$
3 1 eqcomi $⊢ dom ⁡ R = X$
4 dmxpid $⊢ dom ⁡ A × A = A$
5 3 4 ineq12i $⊢ dom ⁡ R ∩ dom ⁡ A × A = X ∩ A$
6 2 5 sseqtri $⊢ dom ⁡ R ∩ A × A ⊆ X ∩ A$
7 6 a1i $⊢ R ∈ PosetRel → dom ⁡ R ∩ A × A ⊆ X ∩ A$
8 simpr $⊢ R ∈ PosetRel ∧ x ∈ X ∩ A → x ∈ X ∩ A$
9 8 elin2d $⊢ R ∈ PosetRel ∧ x ∈ X ∩ A → x ∈ A$
10 elinel1 $⊢ x ∈ X ∩ A → x ∈ X$
11 1 psref $⊢ R ∈ PosetRel ∧ x ∈ X → x R x$
12 10 11 sylan2 $⊢ R ∈ PosetRel ∧ x ∈ X ∩ A → x R x$
13 brinxp2 $⊢ x R ∩ A × A x ↔ x ∈ A ∧ x ∈ A ∧ x R x$
14 9 9 12 13 syl21anbrc $⊢ R ∈ PosetRel ∧ x ∈ X ∩ A → x R ∩ A × A x$
15 vex $⊢ x ∈ V$
16 15 15 breldm $⊢ x R ∩ A × A x → x ∈ dom ⁡ R ∩ A × A$
17 14 16 syl $⊢ R ∈ PosetRel ∧ x ∈ X ∩ A → x ∈ dom ⁡ R ∩ A × A$
18 7 17 eqelssd $⊢ R ∈ PosetRel → dom ⁡ R ∩ A × A = X ∩ A$