brr0d

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

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

Proof

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

Metamath Proof Explorer

Theorem brr0d

Proof