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 \times_{𝑠} S$
	xpsle.x	$⊢ X = {Base}_{R}$
	xpsle.y	$⊢ Y = {Base}_{S}$
	xpsle.1	$⊢ φ \to R \in V$
	xpsle.2	$⊢ φ \to S \in W$
	xpsle.p	$⊢ \underset{˙}{\leq} = \leq_{T}$
	xpsle.m	$⊢ M = \leq_{R}$
	xpsle.n	$⊢ N = \leq_{S}$
	xpsle.3	$⊢ φ \to A \in X$
	xpsle.4	$⊢ φ \to B \in Y$
	xpsle.5	$⊢ φ \to C \in X$
	xpsle.6	$⊢ φ \to D \in Y$
Assertion	xpsle	$⊢ φ \to (⟨A, B⟩ \underset{˙}{\leq} ⟨C, D⟩ \leftrightarrow (A M C \land B N D))$

Proof

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

Metamath Proof Explorer

Theorem xpsle

Proof