Metamath Proof Explorer


Theorem xpsle

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

Ref Expression
Hypotheses xpsle.t 𝑇 = ( 𝑅 ×s 𝑆 )
xpsle.x 𝑋 = ( Base ‘ 𝑅 )
xpsle.y 𝑌 = ( Base ‘ 𝑆 )
xpsle.1 ( 𝜑𝑅𝑉 )
xpsle.2 ( 𝜑𝑆𝑊 )
xpsle.p = ( le ‘ 𝑇 )
xpsle.m 𝑀 = ( le ‘ 𝑅 )
xpsle.n 𝑁 = ( le ‘ 𝑆 )
xpsle.3 ( 𝜑𝐴𝑋 )
xpsle.4 ( 𝜑𝐵𝑌 )
xpsle.5 ( 𝜑𝐶𝑋 )
xpsle.6 ( 𝜑𝐷𝑌 )
Assertion xpsle ( 𝜑 → ( ⟨ 𝐴 , 𝐵𝐶 , 𝐷 ⟩ ↔ ( 𝐴 𝑀 𝐶𝐵 𝑁 𝐷 ) ) )

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 xpsle.m 𝑀 = ( le ‘ 𝑅 )
8 xpsle.n 𝑁 = ( le ‘ 𝑆 )
9 xpsle.3 ( 𝜑𝐴𝑋 )
10 xpsle.4 ( 𝜑𝐵𝑌 )
11 xpsle.5 ( 𝜑𝐶𝑋 )
12 xpsle.6 ( 𝜑𝐷𝑌 )
13 df-ov ( 𝐴 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐵 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
14 eqid ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
15 14 xpsfval ( ( 𝐴𝑋𝐵𝑌 ) → ( 𝐴 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐵 ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
16 9 10 15 syl2anc ( 𝜑 → ( 𝐴 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐵 ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
17 13 16 eqtr3id ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
18 9 10 opelxpd ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) )
19 14 xpsff1o2 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
20 f1of ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
21 19 20 ax-mp ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) ⟶ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
22 21 ffvelrni ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
23 18 22 syl ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
24 17 23 eqeltrrd ( 𝜑 → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
25 df-ov ( 𝐶 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐷 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ )
26 14 xpsfval ( ( 𝐶𝑋𝐷𝑌 ) → ( 𝐶 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐷 ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } )
27 11 12 26 syl2anc ( 𝜑 → ( 𝐶 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) 𝐷 ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } )
28 25 27 eqtr3id ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } )
29 11 12 opelxpd ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) )
30 21 ffvelrni ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
31 29 30 syl ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
32 28 31 eqeltrrd ( 𝜑 → { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
33 eqid ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
34 eqid ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) = ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } )
35 1 2 3 4 5 14 33 34 xpsval ( 𝜑𝑇 = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) “s ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
36 1 2 3 4 5 14 33 34 xpsrnbas ( 𝜑 → ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
37 f1ocnv ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
38 19 37 mp1i ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) )
39 f1ofo ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –1-1-onto→ ( 𝑋 × 𝑌 ) → ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
40 38 39 syl ( 𝜑 ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) –onto→ ( 𝑋 × 𝑌 ) )
41 ovexd ( 𝜑 → ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ∈ V )
42 eqid ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
43 38 f1olecpbl ( ( 𝜑 ∧ ( 𝑎 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ 𝑏 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ∧ ( 𝑐 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ 𝑑 ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) ) → ( ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑎 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑐 ) ∧ ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑏 ) = ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ 𝑑 ) ) → ( 𝑎 ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) 𝑏𝑐 ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) 𝑑 ) ) )
44 35 36 40 41 6 42 43 imasleval ( ( 𝜑 ∧ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ↔ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) )
45 24 32 44 mpd3an23 ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ↔ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) )
46 f1ocnvfv ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ ) )
47 19 18 46 sylancr ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ ) )
48 17 47 mpd ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) = ⟨ 𝐴 , 𝐵 ⟩ )
49 f1ocnvfv ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) : ( 𝑋 × 𝑌 ) –1-1-onto→ ran ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ ) )
50 19 29 49 sylancr ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ ) )
51 28 50 mpd ( 𝜑 → ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) = ⟨ 𝐶 , 𝐷 ⟩ )
52 48 51 breq12d ( 𝜑 → ( ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ) ( ( 𝑥𝑋 , 𝑦𝑌 ↦ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) ‘ { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ) ↔ ⟨ 𝐴 , 𝐵𝐶 , 𝐷 ⟩ ) )
53 eqid ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) = ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) )
54 fvexd ( 𝜑 → ( Scalar ‘ 𝑅 ) ∈ V )
55 2on 2o ∈ On
56 55 a1i ( 𝜑 → 2o ∈ On )
57 fnpr2o ( ( 𝑅𝑉𝑆𝑊 ) → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
58 4 5 57 syl2anc ( 𝜑 → { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } Fn 2o )
59 24 36 eleqtrd ( 𝜑 → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
60 32 36 eleqtrd ( 𝜑 → { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ∈ ( Base ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) )
61 34 53 54 56 58 59 60 42 prdsleval ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ↔ ∀ 𝑘 ∈ 2o ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ) )
62 df2o3 2o = { ∅ , 1o }
63 62 raleqi ( ∀ 𝑘 ∈ 2o ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ { ∅ , 1o } ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) )
64 0ex ∅ ∈ V
65 1oex 1o ∈ V
66 fveq2 ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) )
67 2fveq3 ( 𝑘 = ∅ → ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) )
68 fveq2 ( 𝑘 = ∅ → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) )
69 66 67 68 breq123d ( 𝑘 = ∅ → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ↔ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ) )
70 fveq2 ( 𝑘 = 1o → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) )
71 2fveq3 ( 𝑘 = 1o → ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) = ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) )
72 fveq2 ( 𝑘 = 1o → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) = ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) )
73 70 71 72 breq123d ( 𝑘 = 1o → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ↔ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) )
74 64 65 69 73 ralpr ( ∀ 𝑘 ∈ { ∅ , 1o } ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ↔ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ∧ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) )
75 63 74 bitri ( ∀ 𝑘 ∈ 2o ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ↔ ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ∧ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) )
76 fvpr0o ( 𝐴𝑋 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
77 9 76 syl ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) = 𝐴 )
78 fvpr0o ( 𝑅𝑉 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
79 4 78 syl ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) = 𝑅 )
80 79 fveq2d ( 𝜑 → ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) = ( le ‘ 𝑅 ) )
81 80 7 eqtr4di ( 𝜑 → ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) = 𝑀 )
82 fvpr0o ( 𝐶𝑋 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) = 𝐶 )
83 11 82 syl ( 𝜑 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) = 𝐶 )
84 77 81 83 breq123d ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ↔ 𝐴 𝑀 𝐶 ) )
85 fvpr1o ( 𝐵𝑌 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) = 𝐵 )
86 10 85 syl ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) = 𝐵 )
87 fvpr1o ( 𝑆𝑊 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
88 5 87 syl ( 𝜑 → ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) = 𝑆 )
89 88 fveq2d ( 𝜑 → ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) = ( le ‘ 𝑆 ) )
90 89 8 eqtr4di ( 𝜑 → ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) = 𝑁 )
91 fvpr1o ( 𝐷𝑌 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) = 𝐷 )
92 12 91 syl ( 𝜑 → ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) = 𝐷 )
93 86 90 92 breq123d ( 𝜑 → ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ↔ 𝐵 𝑁 𝐷 ) )
94 84 93 anbi12d ( 𝜑 → ( ( ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ ∅ ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ ∅ ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ ∅ ) ∧ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 1o ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 1o ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 1o ) ) ↔ ( 𝐴 𝑀 𝐶𝐵 𝑁 𝐷 ) ) )
95 75 94 syl5bb ( 𝜑 → ( ∀ 𝑘 ∈ 2o ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ‘ 𝑘 ) ( le ‘ ( { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ‘ 𝑘 ) ) ( { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ‘ 𝑘 ) ↔ ( 𝐴 𝑀 𝐶𝐵 𝑁 𝐷 ) ) )
96 61 95 bitrd ( 𝜑 → ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ( le ‘ ( ( Scalar ‘ 𝑅 ) Xs { ⟨ ∅ , 𝑅 ⟩ , ⟨ 1o , 𝑆 ⟩ } ) ) { ⟨ ∅ , 𝐶 ⟩ , ⟨ 1o , 𝐷 ⟩ } ↔ ( 𝐴 𝑀 𝐶𝐵 𝑁 𝐷 ) ) )
97 45 52 96 3bitr3d ( 𝜑 → ( ⟨ 𝐴 , 𝐵𝐶 , 𝐷 ⟩ ↔ ( 𝐴 𝑀 𝐶𝐵 𝑁 𝐷 ) ) )