Theorem brr0d

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

	Ref	Expression
Hypotheses	brr0d.1	$$⊢\phi \to A\in \mathrm{On}$$
	brr0d.2	$$⊢\phi \to B\in \mathrm{On}$$
	brr0d.3	$$⊢\phi \to C\in \mathrm{On}$$
	brr0d.4	$$⊢\phi \to D\in \mathrm{On}$$
Assertion	brr0d	Could not format assertion : No typesetting found for |- ( ph -> ( <. A , B >. _R0 <. C , D >. <-> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		brr0d.1	$$⊢\phi \to A\in \mathrm{On}$$
2		brr0d.2	$$⊢\phi \to B\in \mathrm{On}$$
3		brr0d.3	$$⊢\phi \to C\in \mathrm{On}$$
4		brr0d.4	$$⊢\phi \to D\in \mathrm{On}$$
5	1 2	opelxpd	$$⊢\phi \to ⟨A,B⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
6	3 4	opelxpd	$$⊢\phi \to ⟨C,D⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
7	5 6	jca	$$⊢\phi \to \left(⟨A,B⟩\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge ⟨C,D⟩\in \left(\mathrm{On}\times \mathrm{On}\right)\right)$$
8		df-r0	Could not format _R0 = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) } : No typesetting found for |- _R0 = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) } with typecode |-
9	8	a1i	Could not format ( ph -> _R0 = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) } ) : No typesetting found for |- ( ph -> _R0 = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) ) } ) with typecode |-
10		fveq2	$$⊢x=⟨A,B⟩\to 1^{st}\left(x\right)=1^{st}\left(⟨A,B⟩\right)$$
11		op1stg	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to 1^{st}\left(⟨A,B⟩\right)=A$$
12	1 2 11	syl2anc	$$⊢\phi \to 1^{st}\left(⟨A,B⟩\right)=A$$
13	10 12	sylan9eqr	$$⊢\left(\phi \wedge x=⟨A,B⟩\right)\to 1^{st}\left(x\right)=A$$
14		fveq2	$$⊢x=⟨A,B⟩\to 2^{nd}\left(x\right)=2^{nd}\left(⟨A,B⟩\right)$$
15		op2ndg	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
16	1 2 15	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨A,B⟩\right)=B$$
17	14 16	sylan9eqr	$$⊢\left(\phi \wedge x=⟨A,B⟩\right)\to 2^{nd}\left(x\right)=B$$
18	13 17	uneq12d	$$⊢\left(\phi \wedge x=⟨A,B⟩\right)\to 1^{st}\left(x\right)\cup 2^{nd}\left(x\right)=A\cup B$$
19	18	adantrr	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to 1^{st}\left(x\right)\cup 2^{nd}\left(x\right)=A\cup B$$
20		fveq2	$$⊢y=⟨C,D⟩\to 1^{st}\left(y\right)=1^{st}\left(⟨C,D⟩\right)$$
21		op1stg	$$⊢\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\to 1^{st}\left(⟨C,D⟩\right)=C$$
22	3 4 21	syl2anc	$$⊢\phi \to 1^{st}\left(⟨C,D⟩\right)=C$$
23	20 22	sylan9eqr	$$⊢\left(\phi \wedge y=⟨C,D⟩\right)\to 1^{st}\left(y\right)=C$$
24		fveq2	$$⊢y=⟨C,D⟩\to 2^{nd}\left(y\right)=2^{nd}\left(⟨C,D⟩\right)$$
25		op2ndg	$$⊢\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\to 2^{nd}\left(⟨C,D⟩\right)=D$$
26	3 4 25	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨C,D⟩\right)=D$$
27	24 26	sylan9eqr	$$⊢\left(\phi \wedge y=⟨C,D⟩\right)\to 2^{nd}\left(y\right)=D$$
28	23 27	uneq12d	$$⊢\left(\phi \wedge y=⟨C,D⟩\right)\to 1^{st}\left(y\right)\cup 2^{nd}\left(y\right)=C\cup D$$
29	28	adantrl	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to 1^{st}\left(y\right)\cup 2^{nd}\left(y\right)=C\cup D$$
30	19 29	eleq12d	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\in \left(1^{st}\left(y\right)\cup 2^{nd}\left(y\right)\right)\leftrightarrow A\cup B\in \left(C\cup D\right)\right)$$
31	19 29	eqeq12d	$$⊢\left(\phi \wedge \left(x=⟨A,B⟩\wedge y=⟨C,D⟩\right)\right)\to \left(1^{st}\left(x\right)\cup 2^{nd}\left(x\right)=1^{st}\left(y\right)\cup 2^{nd}\left(y\right)\leftrightarrow A\cup B=C\cup D\right)$$
32		breq12	Could not format ( ( x = <. A , B >. /\ y = <. C , D >. ) -> ( x LexOrd y <-> <. A , B >. LexOrd <. C , D >. ) ) : No typesetting found for |- ( ( x = <. A , B >. /\ y = <. C , D >. ) -> ( x LexOrd y <-> <. A , B >. LexOrd <. C , D >. ) ) with typecode |-
33	32	adantl	Could not format ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( x LexOrd y <-> <. A , B >. LexOrd <. C , D >. ) ) : No typesetting found for |- ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( x LexOrd y <-> <. A , B >. LexOrd <. C , D >. ) ) with typecode |-
34	31 33	anbi12d	Could not format ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) <-> ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) : No typesetting found for |- ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) <-> ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) with typecode |-
35	30 34	orbi12d	Could not format ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) <-> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) : No typesetting found for |- ( ( ph /\ ( x = <. A , B >. /\ y = <. C , D >. ) ) -> ( ( ( ( 1st ` x ) u. ( 2nd ` x ) ) e. ( ( 1st ` y ) u. ( 2nd ` y ) ) \/ ( ( ( 1st ` x ) u. ( 2nd ` x ) ) = ( ( 1st ` y ) u. ( 2nd ` y ) ) /\ x LexOrd y ) ) <-> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) with typecode |-
36	9 35	brab2d	Could not format ( ph -> ( <. A , B >. _R0 <. C , D >. <-> ( ( <. A , B >. e. ( On X. On ) /\ <. C , D >. e. ( On X. On ) ) /\ ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) ) : No typesetting found for |- ( ph -> ( <. A , B >. _R0 <. C , D >. <-> ( ( <. A , B >. e. ( On X. On ) /\ <. C , D >. e. ( On X. On ) ) /\ ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) ) with typecode |-
37	7 36	mpbirand	Could not format ( ph -> ( <. A , B >. _R0 <. C , D >. <-> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) : No typesetting found for |- ( ph -> ( <. A , B >. _R0 <. C , D >. <-> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) with typecode |-