This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brdifun

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

		Ref	Expression
	Hypothesis	swoer.1	⊢ 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ^◡ < ) )
	Assertion	brdifun	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		swoer.1	⊢ 𝑅 = ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ^◡ < ) )
2		opelxpi	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) )
3		df-br	⊢ ( 𝐴 ( 𝑋 × 𝑋 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑋 ) )
4	2 3	sylibr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ( 𝑋 × 𝑋 ) 𝐵 )
5	1	breqi	⊢ ( 𝐴 𝑅 𝐵 ↔ 𝐴 ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ^◡ < ) ) 𝐵 )
6		brdif	⊢ ( 𝐴 ( ( 𝑋 × 𝑋 ) ∖ ( < ∪ ^◡ < ) ) 𝐵 ↔ ( 𝐴 ( 𝑋 × 𝑋 ) 𝐵 ∧ ¬ 𝐴 ( < ∪ ^◡ < ) 𝐵 ) )
7	5 6	bitri	⊢ ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 ( 𝑋 × 𝑋 ) 𝐵 ∧ ¬ 𝐴 ( < ∪ ^◡ < ) 𝐵 ) )
8	7	baib	⊢ ( 𝐴 ( 𝑋 × 𝑋 ) 𝐵 → ( 𝐴 𝑅 𝐵 ↔ ¬ 𝐴 ( < ∪ ^◡ < ) 𝐵 ) )
9	4 8	syl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ↔ ¬ 𝐴 ( < ∪ ^◡ < ) 𝐵 ) )
10		brun	⊢ ( 𝐴 ( < ∪ ^◡ < ) 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐴 ^◡ < 𝐵 ) )
11		brcnvg	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ^◡ < 𝐵 ↔ 𝐵 < 𝐴 ) )
12	11	orbi2d	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 < 𝐵 ∨ 𝐴 ^◡ < 𝐵 ) ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
13	10 12	bitrid	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( < ∪ ^◡ < ) 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
14	13	notbid	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ¬ 𝐴 ( < ∪ ^◡ < ) 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )
15	9 14	bitrd	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ) )