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

Metamath Proof Explorer

Theorem brsdom2

Description: Alternate definition of strict dominance. Definition 3 of Suppes p. 97. (Contributed by NM, 27-Jul-2004)

Ref Expression
Hypotheses brsdom2.1 ⊢ 𝐴 ∈ V
brsdom2.2 ⊢ 𝐵 ∈ V
Assertion brsdom2 ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 brsdom2.1 ⊢ 𝐴 ∈ V
2 brsdom2.2 ⊢ 𝐵 ∈ V
3 dfsdom2 ⊢ ≺ = ( ≼ ∖ ◡ ≼ )
4 3 eleq2i ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ◡ ≼ ) )
5 df-br ⊢ ( 𝐴 ≺ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ )
6 df-br ⊢ ( 𝐴 ≼ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ )
7 df-br ⊢ ( 𝐵 ≼ 𝐴 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ ≼ )
8 1 2 opelcnv ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ ≼ )
9 7 8 bitr4i ⊢ ( 𝐵 ≼ 𝐴 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ )
10 9 notbii ⊢ ( ¬ 𝐵 ≼ 𝐴 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ )
11 6 10 anbi12i ⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ ) )
12 eldif ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ◡ ≼ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ ) )
13 11 12 bitr4i ⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ◡ ≼ ) )
14 4 5 13 3bitr4i ⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴 ) )