Theorem elovconstbrd

Description: Two ways of expressing A R B . (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypotheses	ovconstbrd.1	$$⊢\phi \to F=R\times \left\{Y\right\}$$
	elovconstbrd.2	$$⊢\phi \to X\in \left(AFB\right)$$
Assertion	elovconstbrd	$$⊢\phi \to ARB$$

Proof

Step	Hyp	Ref	Expression
1		ovconstbrd.1	$$⊢\phi \to F=R\times \left\{Y\right\}$$
2		elovconstbrd.2	$$⊢\phi \to X\in \left(AFB\right)$$
3	2	ne0d	$$⊢\phi \to AFB\ne \varnothing$$
4	1	oveqd	$$⊢\phi \to AFB=A\left(R\times \left\{Y\right\}\right)B$$
5		df-ov	$$⊢A\left(R\times \left\{Y\right\}\right)B=\left(R\times \left\{Y\right\}\right)\left(⟨A,B⟩\right)$$
6	4 5	eqtrdi	$$⊢\phi \to AFB=\left(R\times \left\{Y\right\}\right)\left(⟨A,B⟩\right)$$
7	6	neeq1d	$$⊢\phi \to \left(AFB\ne \varnothing \leftrightarrow \left(R\times \left\{Y\right\}\right)\left(⟨A,B⟩\right)\ne \varnothing \right)$$
8		dmxpss	$$⊢\mathrm{dom}\left(R\times \left\{Y\right\}\right)\subseteq R$$
9		ndmfv	$$⊢\neg ⟨A,B⟩\in \mathrm{dom}\left(R\times \left\{Y\right\}\right)\to \left(R\times \left\{Y\right\}\right)\left(⟨A,B⟩\right)=\varnothing$$
10	9	necon1ai	$$⊢\left(R\times \left\{Y\right\}\right)\left(⟨A,B⟩\right)\ne \varnothing \to ⟨A,B⟩\in \mathrm{dom}\left(R\times \left\{Y\right\}\right)$$
11	8 10	sselid	$$⊢\left(R\times \left\{Y\right\}\right)\left(⟨A,B⟩\right)\ne \varnothing \to ⟨A,B⟩\in R$$
12	7 11	biimtrdi	$$⊢\phi \to \left(AFB\ne \varnothing \to ⟨A,B⟩\in R\right)$$
13	3 12	mpd	$$⊢\phi \to ⟨A,B⟩\in R$$
14		df-br	$$⊢ARB\leftrightarrow ⟨A,B⟩\in R$$
15	13 14	sylibr	$$⊢\phi \to ARB$$