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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ≤ ⊆ ( 𝐵 × 𝐵 ) )