Theorem prsss

Description: Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018)

	Ref	Expression
Hypotheses	ordtNEW.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	ordtNEW.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
Assertion	prsss	⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordtNEW.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		ordtNEW.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3	2	ineq1i	⊢ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ∩ ( 𝐴 × 𝐴 ) )
4		inass	⊢ ( ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( ( 𝐵 × 𝐵 ) ∩ ( 𝐴 × 𝐴 ) ) )
5	3 4	eqtri	⊢ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( ( 𝐵 × 𝐵 ) ∩ ( 𝐴 × 𝐴 ) ) )
6		xpss12	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 × 𝐴 ) ⊆ ( 𝐵 × 𝐵 ) )
7	6	anidms	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 × 𝐴 ) ⊆ ( 𝐵 × 𝐵 ) )
8		sseqin2	⊢ ( ( 𝐴 × 𝐴 ) ⊆ ( 𝐵 × 𝐵 ) ↔ ( ( 𝐵 × 𝐵 ) ∩ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
9	7 8	sylib	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝐵 × 𝐵 ) ∩ ( 𝐴 × 𝐴 ) ) = ( 𝐴 × 𝐴 ) )
10	9	ineq2d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( le ‘ 𝐾 ) ∩ ( ( 𝐵 × 𝐵 ) ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )
11	5 10	syl5eq	⊢ ( 𝐴 ⊆ 𝐵 → ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )
12	11	adantl	⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )