xporderlem

Description: Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011)

		Ref	Expression
	Hypothesis	xporderlem.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) }
	Assertion	xporderlem	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xporderlem.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) }
2		df-br	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ↔ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∈ 𝑇 )
3	1	eleq2i	⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∈ 𝑇 ↔ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) } )
4	2 3	bitri	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ↔ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) } )
5		opex	⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
6		opex	⊢ ⟨ 𝑐 , 𝑑 ⟩ ∈ V
7		eleq1	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
8		opelxp	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) )
9	7 8	bitrdi	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) )
10	9	anbi1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ) )
11		vex	⊢ 𝑎 ∈ V
12		vex	⊢ 𝑏 ∈ V
13	11 12	op1std	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1^st ‘ 𝑥 ) = 𝑎 )
14	13	breq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ↔ 𝑎 𝑅 ( 1^st ‘ 𝑦 ) ) )
15	13	eqeq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ↔ 𝑎 = ( 1^st ‘ 𝑦 ) ) )
16	11 12	op2ndd	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2^nd ‘ 𝑥 ) = 𝑏 )
17	16	breq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ↔ 𝑏 𝑆 ( 2^nd ‘ 𝑦 ) ) )
18	15 17	anbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ↔ ( 𝑎 = ( 1^st ‘ 𝑦 ) ∧ 𝑏 𝑆 ( 2^nd ‘ 𝑦 ) ) ) )
19	14 18	orbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ↔ ( 𝑎 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( 𝑎 = ( 1^st ‘ 𝑦 ) ∧ 𝑏 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) )
20	10 19	anbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( 𝑎 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( 𝑎 = ( 1^st ‘ 𝑦 ) ∧ 𝑏 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) ) )
21		eleq1	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑦 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
22		opelxp	⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) )
23	21 22	bitrdi	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑦 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) )
24	23	anbi2d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ) )
25		vex	⊢ 𝑐 ∈ V
26		vex	⊢ 𝑑 ∈ V
27	25 26	op1std	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 1^st ‘ 𝑦 ) = 𝑐 )
28	27	breq2d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑎 𝑅 ( 1^st ‘ 𝑦 ) ↔ 𝑎 𝑅 𝑐 ) )
29	27	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑎 = ( 1^st ‘ 𝑦 ) ↔ 𝑎 = 𝑐 ) )
30	25 26	op2ndd	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 2^nd ‘ 𝑦 ) = 𝑑 )
31	30	breq2d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑏 𝑆 ( 2^nd ‘ 𝑦 ) ↔ 𝑏 𝑆 𝑑 ) )
32	29 31	anbi12d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑎 = ( 1^st ‘ 𝑦 ) ∧ 𝑏 𝑆 ( 2^nd ‘ 𝑦 ) ) ↔ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) )
33	28 32	orbi12d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑎 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( 𝑎 = ( 1^st ‘ 𝑦 ) ∧ 𝑏 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ↔ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) )
34	24 33	anbi12d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( 𝑎 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( 𝑎 = ( 1^st ‘ 𝑦 ) ∧ 𝑏 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ) )
35	5 6 20 34	opelopab	⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) } ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) )
36		an4	⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) )
37	36	anbi1i	⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) )
38	4 35 37	3bitri	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) )

Metamath Proof Explorer

Theorem xporderlem

Proof