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

Metamath Proof Explorer

Theorem xpsle

Proof