Theorem brnonrel

Description: A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020)

	Ref	Expression
Assertion	brnonrel	$$⊢\left(X\in U\wedge Y\in V\right)\to \neg X\left(A\setminus {A^{-1}}^{-1}\right)Y$$

Proof

Step	Hyp	Ref	Expression
1		br0	$$⊢\neg Y\varnothing X$$
2		brcnvg	$$⊢\left(Y\in V\wedge X\in U\right)\to \left(Y{\left(A\setminus {A^{-1}}^{-1}\right)}^{-1}X\leftrightarrow X\left(A\setminus {A^{-1}}^{-1}\right)Y\right)$$
3	2	ancoms	$$⊢\left(X\in U\wedge Y\in V\right)\to \left(Y{\left(A\setminus {A^{-1}}^{-1}\right)}^{-1}X\leftrightarrow X\left(A\setminus {A^{-1}}^{-1}\right)Y\right)$$
4		cnvnonrel	$$⊢{\left(A\setminus {A^{-1}}^{-1}\right)}^{-1}=\varnothing$$
5	4	breqi	$$⊢Y{\left(A\setminus {A^{-1}}^{-1}\right)}^{-1}X\leftrightarrow Y\varnothing X$$
6	3 5	bitr3di	$$⊢\left(X\in U\wedge Y\in V\right)\to \left(X\left(A\setminus {A^{-1}}^{-1}\right)Y\leftrightarrow Y\varnothing X\right)$$
7	1 6	mtbiri	$$⊢\left(X\in U\wedge Y\in V\right)\to \neg X\left(A\setminus {A^{-1}}^{-1}\right)Y$$