Theorem brdifun

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

	Ref	Expression
Hypothesis	swoer.1	|- R = ( ( X X. X ) \ ( .< u. `' .< ) )
Assertion	brdifun	|- ( ( A e. X /\ B e. X ) -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )

Proof

Step	Hyp	Ref	Expression
1		swoer.1	|- R = ( ( X X. X ) \ ( .< u. `' .< ) )
2		opelxpi	|- ( ( A e. X /\ B e. X ) -> <. A , B >. e. ( X X. X ) )
3		df-br	|- ( A ( X X. X ) B <-> <. A , B >. e. ( X X. X ) )
4	2 3	sylibr	|- ( ( A e. X /\ B e. X ) -> A ( X X. X ) B )
5	1	breqi	|- ( A R B <-> A ( ( X X. X ) \ ( .< u. `' .< ) ) B )
6		brdif	|- ( A ( ( X X. X ) \ ( .< u. `' .< ) ) B <-> ( A ( X X. X ) B /\ -. A ( .< u. `' .< ) B ) )
7	5 6	bitri	|- ( A R B <-> ( A ( X X. X ) B /\ -. A ( .< u. `' .< ) B ) )
8	7	baib	|- ( A ( X X. X ) B -> ( A R B <-> -. A ( .< u. `' .< ) B ) )
9	4 8	syl	|- ( ( A e. X /\ B e. X ) -> ( A R B <-> -. A ( .< u. `' .< ) B ) )
10		brun	|- ( A ( .< u. `' .< ) B <-> ( A .< B \/ A `' .< B ) )
11		brcnvg	|- ( ( A e. X /\ B e. X ) -> ( A `' .< B <-> B .< A ) )
12	11	orbi2d	|- ( ( A e. X /\ B e. X ) -> ( ( A .< B \/ A `' .< B ) <-> ( A .< B \/ B .< A ) ) )
13	10 12	syl5bb	|- ( ( A e. X /\ B e. X ) -> ( A ( .< u. `' .< ) B <-> ( A .< B \/ B .< A ) ) )
14	13	notbid	|- ( ( A e. X /\ B e. X ) -> ( -. A ( .< u. `' .< ) B <-> -. ( A .< B \/ B .< A ) ) )
15	9 14	bitrd	|- ( ( A e. X /\ B e. X ) -> ( A R B <-> -. ( A .< B \/ B .< A ) ) )