Theorem brlexod

Description: Condition for two ordered pairs to be related by LexOrd . (Contributed by BTernaryTau, 20-Sep-2026)

	Ref	Expression
Hypotheses	brlexod.1	⊢ ( 𝜑 → 𝐴 ∈ On )
	brlexod.2	⊢ ( 𝜑 → 𝐵 ∈ On )
	brlexod.3	⊢ ( 𝜑 → 𝐶 ∈ On )
	brlexod.4	⊢ ( 𝜑 → 𝐷 ∈ On )
Assertion	brlexod	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ LexOrd ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ∈ 𝐶 ∨ ( 𝐴 = 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		brlexod.1	⊢ ( 𝜑 → 𝐴 ∈ On )
2		brlexod.2	⊢ ( 𝜑 → 𝐵 ∈ On )
3		brlexod.3	⊢ ( 𝜑 → 𝐶 ∈ On )
4		brlexod.4	⊢ ( 𝜑 → 𝐷 ∈ On )
5	1 2	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) )
6	3 4	opelxpd	⊢ ( 𝜑 → ⟨ 𝐶 , 𝐷 ⟩ ∈ ( On × On ) )
7	5 6	jca	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( On × On ) ) )
8		df-lexo	⊢ LexOrd = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) }
9	8	a1i	⊢ ( 𝜑 → LexOrd = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ) } )
10		fveq2	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 1st ‘ 𝑥 ) = ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
11		op1stg	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
12	1 2 11	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
13	10 12	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 1st ‘ 𝑥 ) = 𝐴 )
14	13	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( 1st ‘ 𝑥 ) = 𝐴 )
15		fveq2	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 1st ‘ 𝑦 ) = ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
16		op1stg	⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
17	3 4 16	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐶 )
18	15 17	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) → ( 1st ‘ 𝑦 ) = 𝐶 )
19	18	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( 1st ‘ 𝑦 ) = 𝐶 )
20	14 19	eleq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ↔ 𝐴 ∈ 𝐶 ) )
21	14 19	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ↔ 𝐴 = 𝐶 ) )
22		fveq2	⊢ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
23		op2ndg	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
24	1 2 23	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
25	22 24	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 2nd ‘ 𝑥 ) = 𝐵 )
26	25	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( 2nd ‘ 𝑥 ) = 𝐵 )
27		fveq2	⊢ ( 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ → ( 2nd ‘ 𝑦 ) = ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) )
28		op2ndg	⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
29	3 4 28	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐶 , 𝐷 ⟩ ) = 𝐷 )
30	27 29	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) → ( 2nd ‘ 𝑦 ) = 𝐷 )
31	30	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( 2nd ‘ 𝑦 ) = 𝐷 )
32	26 31	eleq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ↔ 𝐵 ∈ 𝐷 ) )
33	21 32	anbi12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) )
34	20 33	orbi12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑦 = ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ( ( 1st ‘ 𝑥 ) ∈ ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) ∈ ( 2nd ‘ 𝑦 ) ) ) ↔ ( 𝐴 ∈ 𝐶 ∨ ( 𝐴 = 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) ) )
35	9 34	brab2d	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ LexOrd ⟨ 𝐶 , 𝐷 ⟩ ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) ∧ ⟨ 𝐶 , 𝐷 ⟩ ∈ ( On × On ) ) ∧ ( 𝐴 ∈ 𝐶 ∨ ( 𝐴 = 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) ) ) )
36	7 35	mpbirand	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ LexOrd ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 ∈ 𝐶 ∨ ( 𝐴 = 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) ) )