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

Metamath Proof Explorer

Theorem psssdm2

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

Ref Expression
Hypothesis psssdm.1 ⊢ 𝑋 = dom 𝑅
Assertion psssdm2 ( 𝑅 ∈ PosetRel → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( 𝑋 ∩ 𝐴 ) )

Proof

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