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 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( 𝑋 ∩ 𝐴 ) )