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 
|- T = ( R Xs. S )
xpsle.x 
|- X = ( Base ` R )
xpsle.y 
|- Y = ( Base ` S )
xpsle.1 
|- ( ph -> R e. V )
xpsle.2 
|- ( ph -> S e. W )
xpsle.p 
|- .<_ = ( le ` T )
xpsle.m 
|- M = ( le ` R )
xpsle.n 
|- N = ( le ` S )
xpsle.3 
|- ( ph -> A e. X )
xpsle.4 
|- ( ph -> B e. Y )
xpsle.5 
|- ( ph -> C e. X )
xpsle.6 
|- ( ph -> D e. Y )
Assertion xpsle 
|- ( ph -> ( <. A , B >. .<_ <. C , D >. <-> ( A M C /\ B N D ) ) )

Proof

Step Hyp Ref Expression
1 xpsle.t 
 |-  T = ( R Xs. S )
2 xpsle.x 
 |-  X = ( Base ` R )
3 xpsle.y 
 |-  Y = ( Base ` S )
4 xpsle.1 
 |-  ( ph -> R e. V )
5 xpsle.2 
 |-  ( ph -> S e. W )
6 xpsle.p 
 |-  .<_ = ( le ` T )
7 xpsle.m 
 |-  M = ( le ` R )
8 xpsle.n 
 |-  N = ( le ` S )
9 xpsle.3 
 |-  ( ph -> A e. X )
10 xpsle.4 
 |-  ( ph -> B e. Y )
11 xpsle.5 
 |-  ( ph -> C e. X )
12 xpsle.6 
 |-  ( ph -> D e. Y )
13 df-ov 
 |-  ( A ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) B ) = ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. )
14 eqid 
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
15 14 xpsfval 
 |-  ( ( A e. X /\ B e. Y ) -> ( A ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) B ) = { <. (/) , A >. , <. 1o , B >. } )
16 9 10 15 syl2anc 
 |-  ( ph -> ( A ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) B ) = { <. (/) , A >. , <. 1o , B >. } )
17 13 16 eqtr3id 
 |-  ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } )
18 9 10 opelxpd 
 |-  ( ph -> <. A , B >. e. ( X X. Y ) )
19 14 xpsff1o2 
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
20 f1of 
 |-  ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -> ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) --> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
21 19 20 ax-mp 
 |-  ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) --> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
22 21 ffvelrni 
 |-  ( <. A , B >. e. ( X X. Y ) -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
23 18 22 syl 
 |-  ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
24 17 23 eqeltrrd 
 |-  ( ph -> { <. (/) , A >. , <. 1o , B >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
25 df-ov 
 |-  ( C ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) D ) = ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. )
26 14 xpsfval 
 |-  ( ( C e. X /\ D e. Y ) -> ( C ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) D ) = { <. (/) , C >. , <. 1o , D >. } )
27 11 12 26 syl2anc 
 |-  ( ph -> ( C ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) D ) = { <. (/) , C >. , <. 1o , D >. } )
28 25 27 eqtr3id 
 |-  ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } )
29 11 12 opelxpd 
 |-  ( ph -> <. C , D >. e. ( X X. Y ) )
30 21 ffvelrni 
 |-  ( <. C , D >. e. ( X X. Y ) -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
31 29 30 syl 
 |-  ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
32 28 31 eqeltrrd 
 |-  ( ph -> { <. (/) , C >. , <. 1o , D >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
33 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
34 eqid 
 |-  ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } )
35 1 2 3 4 5 14 33 34 xpsval 
 |-  ( ph -> T = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
36 1 2 3 4 5 14 33 34 xpsrnbas 
 |-  ( ph -> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
37 f1ocnv 
 |-  ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) )
38 19 37 mp1i 
 |-  ( ph -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) )
39 f1ofo 
 |-  ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -onto-> ( X X. Y ) )
40 38 39 syl 
 |-  ( ph -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -onto-> ( X X. Y ) )
41 ovexd 
 |-  ( ph -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V )
42 eqid 
 |-  ( le ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( le ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
43 38 f1olecpbl 
 |-  ( ( ph /\ ( a e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ b e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) /\ ( c e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ d e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) -> ( ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` a ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` c ) /\ ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` b ) = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` d ) ) -> ( a ( le ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) b <-> c ( le ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) d ) ) )
44 35 36 40 41 6 42 43 imasleval 
 |-  ( ( ph /\ { <. (/) , A >. , <. 1o , B >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ { <. (/) , C >. , <. 1o , D >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) -> ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) .<_ ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) <-> { <. (/) , A >. , <. 1o , B >. } ( le ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } ) )
45 24 32 44 mpd3an23 
 |-  ( ph -> ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) .<_ ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) <-> { <. (/) , A >. , <. 1o , B >. } ( le ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } ) )
46 f1ocnvfv 
 |-  ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ <. A , B >. e. ( X X. Y ) ) -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. ) )
47 19 18 46 sylancr 
 |-  ( ph -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. ) )
48 17 47 mpd 
 |-  ( ph -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. )
49 f1ocnvfv 
 |-  ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ <. C , D >. e. ( X X. Y ) ) -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. ) )
50 19 29 49 sylancr 
 |-  ( ph -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. ) )
51 28 50 mpd 
 |-  ( ph -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. )
52 48 51 breq12d 
 |-  ( ph -> ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) .<_ ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) <-> <. A , B >. .<_ <. C , D >. ) )
53 eqid 
 |-  ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
54 fvexd 
 |-  ( ph -> ( Scalar ` R ) e. _V )
55 2on 
 |-  2o e. On
56 55 a1i 
 |-  ( ph -> 2o e. On )
57 fnpr2o 
 |-  ( ( R e. V /\ S e. W ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
58 4 5 57 syl2anc 
 |-  ( ph -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
59 24 36 eleqtrd 
 |-  ( ph -> { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
60 32 36 eleqtrd 
 |-  ( ph -> { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
61 34 53 54 56 58 59 60 42 prdsleval 
 |-  ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ( le ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } <-> A. k e. 2o ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) )
62 df2o3 
 |-  2o = { (/) , 1o }
63 62 raleqi 
 |-  ( A. k e. 2o ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) <-> A. k e. { (/) , 1o } ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) )
64 0ex 
 |-  (/) e. _V
65 1oex 
 |-  1o e. _V
66 fveq2 
 |-  ( k = (/) -> ( { <. (/) , A >. , <. 1o , B >. } ` k ) = ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) )
67 2fveq3 
 |-  ( k = (/) -> ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) )
68 fveq2 
 |-  ( k = (/) -> ( { <. (/) , C >. , <. 1o , D >. } ` k ) = ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) )
69 66 67 68 breq123d 
 |-  ( k = (/) -> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) <-> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) )
70 fveq2 
 |-  ( k = 1o -> ( { <. (/) , A >. , <. 1o , B >. } ` k ) = ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) )
71 2fveq3 
 |-  ( k = 1o -> ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) )
72 fveq2 
 |-  ( k = 1o -> ( { <. (/) , C >. , <. 1o , D >. } ` k ) = ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) )
73 70 71 72 breq123d 
 |-  ( k = 1o -> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) <-> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) )
74 64 65 69 73 ralpr 
 |-  ( A. k e. { (/) , 1o } ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) <-> ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) /\ ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) )
75 63 74 bitri 
 |-  ( A. k e. 2o ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) <-> ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) /\ ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) )
76 fvpr0o 
 |-  ( A e. X -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A )
77 9 76 syl 
 |-  ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A )
78 fvpr0o 
 |-  ( R e. V -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R )
79 4 78 syl 
 |-  ( ph -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R )
80 79 fveq2d 
 |-  ( ph -> ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) = ( le ` R ) )
81 80 7 eqtr4di 
 |-  ( ph -> ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) = M )
82 fvpr0o 
 |-  ( C e. X -> ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) = C )
83 11 82 syl 
 |-  ( ph -> ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) = C )
84 77 81 83 breq123d 
 |-  ( ph -> ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) <-> A M C ) )
85 fvpr1o 
 |-  ( B e. Y -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B )
86 10 85 syl 
 |-  ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B )
87 fvpr1o 
 |-  ( S e. W -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S )
88 5 87 syl 
 |-  ( ph -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S )
89 88 fveq2d 
 |-  ( ph -> ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) = ( le ` S ) )
90 89 8 eqtr4di 
 |-  ( ph -> ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) = N )
91 fvpr1o 
 |-  ( D e. Y -> ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) = D )
92 12 91 syl 
 |-  ( ph -> ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) = D )
93 86 90 92 breq123d 
 |-  ( ph -> ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) <-> B N D ) )
94 84 93 anbi12d 
 |-  ( ph -> ( ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) /\ ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) <-> ( A M C /\ B N D ) ) )
95 75 94 syl5bb 
 |-  ( ph -> ( A. k e. 2o ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( le ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) <-> ( A M C /\ B N D ) ) )
96 61 95 bitrd 
 |-  ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ( le ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } <-> ( A M C /\ B N D ) ) )
97 45 52 96 3bitr3d 
 |-  ( ph -> ( <. A , B >. .<_ <. C , D >. <-> ( A M C /\ B N D ) ) )