Theorem brdifun

Description: Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Hypothesis	swoer.1	$$⊢R=\left(X\times X\right)\setminus \left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)$$
Assertion	brdifun	$$⊢\left(A\in X\wedge B\in X\right)\to \left(ARB\leftrightarrow \neg \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		swoer.1	$$⊢R=\left(X\times X\right)\setminus \left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)$$
2		opelxpi	$$⊢\left(A\in X\wedge B\in X\right)\to ⟨A,B⟩\in \left(X\times X\right)$$
3		df-br	$$⊢A\left(X\times X\right)B\leftrightarrow ⟨A,B⟩\in \left(X\times X\right)$$
4	2 3	sylibr	$$⊢\left(A\in X\wedge B\in X\right)\to A\left(X\times X\right)B$$
5	1	breqi	$$⊢ARB\leftrightarrow A\left(\left(X\times X\right)\setminus \left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)\right)B$$
6		brdif	$$⊢A\left(\left(X\times X\right)\setminus \left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)\right)B\leftrightarrow \left(A\left(X\times X\right)B\wedge \neg A\left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)B\right)$$
7	5 6	bitri	$$⊢ARB\leftrightarrow \left(A\left(X\times X\right)B\wedge \neg A\left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)B\right)$$
8	7	baib	$$⊢A\left(X\times X\right)B\to \left(ARB\leftrightarrow \neg A\left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)B\right)$$
9	4 8	syl	$$⊢\left(A\in X\wedge B\in X\right)\to \left(ARB\leftrightarrow \neg A\left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)B\right)$$
10		brun	$$⊢A\left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)B\leftrightarrow \left(A\underset{\dot{}}{<}B\vee A{\underset{\dot{}}{<}}^{-1}B\right)$$
11		brcnvg	$$⊢\left(A\in X\wedge B\in X\right)\to \left(A{\underset{\dot{}}{<}}^{-1}B\leftrightarrow B\underset{\dot{}}{<}A\right)$$
12	11	orbi2d	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\left(A\underset{\dot{}}{<}B\vee A{\underset{\dot{}}{<}}^{-1}B\right)\leftrightarrow \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)\right)$$
13	10 12	syl5bb	$$⊢\left(A\in X\wedge B\in X\right)\to \left(A\left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)B\leftrightarrow \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)\right)$$
14	13	notbid	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\neg A\left(\underset{\dot{}}{<}\cup {\underset{\dot{}}{<}}^{-1}\right)B\leftrightarrow \neg \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)\right)$$
15	9 14	bitrd	$$⊢\left(A\in X\wedge B\in X\right)\to \left(ARB\leftrightarrow \neg \left(A\underset{\dot{}}{<}B\vee B\underset{\dot{}}{<}A\right)\right)$$