Theorem prdsless

Description: Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015)

	Ref	Expression
Hypotheses	prdsbas.p	⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
	prdsbas.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
	prdsbas.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	prdsbas.i	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
	prdsle.l	⊢ ≤ = ( le ‘ 𝑃 )
Assertion	prdsless	⊢ ( 𝜑 → ≤ ⊆ ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		prdsbas.p	⊢ 𝑃 = ( 𝑆 Xs 𝑅 )
2		prdsbas.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3		prdsbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
4		prdsbas.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		prdsbas.i	⊢ ( 𝜑 → dom 𝑅 = 𝐼 )
6		prdsle.l	⊢ ≤ = ( le ‘ 𝑃 )
7	1 2 3 4 5 6	prdsle	⊢ ( 𝜑 → ≤ = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } )
8		vex	⊢ 𝑓 ∈ V
9		vex	⊢ 𝑔 ∈ V
10	8 9	prss	⊢ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ↔ { 𝑓 , 𝑔 } ⊆ 𝐵 )
11	10	anbi1i	⊢ ( ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) ↔ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) )
12	11	opabbii	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) }
13		opabssxp	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⊆ ( 𝐵 × 𝐵 )
14	12 13	eqsstrri	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( { 𝑓 , 𝑔 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ( le ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝑔 ‘ 𝑥 ) ) } ⊆ ( 𝐵 × 𝐵 )
15	7 14	eqsstrdi	⊢ ( 𝜑 → ≤ ⊆ ( 𝐵 × 𝐵 ) )