Metamath Proof Explorer


Theorem xpsless

Description: Closure of the ordering in a binary structure product. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses xpsle.t 𝑇 = ( 𝑅 ×s 𝑆 )
xpsle.x 𝑋 = ( Base ‘ 𝑅 )
xpsle.y 𝑌 = ( Base ‘ 𝑆 )
xpsle.1 ( 𝜑𝑅𝑉 )
xpsle.2 ( 𝜑𝑆𝑊 )
xpsle.p = ( le ‘ 𝑇 )
Assertion xpsless ( 𝜑 ⊆ ( ( 𝑋 × 𝑌 ) × ( 𝑋 × 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 xpsle.t 𝑇 = ( 𝑅 ×s 𝑆 )
2 xpsle.x 𝑋 = ( Base ‘ 𝑅 )
3 xpsle.y 𝑌 = ( Base ‘ 𝑆 )
4 xpsle.1 ( 𝜑𝑅𝑉 )
5 xpsle.2 ( 𝜑𝑆𝑊 )
6 xpsle.p = ( le ‘ 𝑇 )
7 eqid ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
8 eqid ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
9 eqid ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
10 1 2 3 4 5 7 8 9 xpsval ( 𝜑𝑇 = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
11 1 2 3 4 5 7 8 9 xpsrnbas ( 𝜑 → ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
12 7 xpsff1o2 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
13 f1ocnv ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
14 12 13 mp1i ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
15 f1ofo ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
16 14 15 syl ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
17 ovexd ( 𝜑 → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
18 10 11 16 17 6 imasless ( 𝜑 ⊆ ( ( 𝑋 × 𝑌 ) × ( 𝑋 × 𝑌 ) ) )