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 ⊢ A ∈ V
brsdom2.2 ⊢ B ∈ V
Assertion brsdom2 ⊢ A ≺ B ↔ A ≼ B ∧ ¬ B ≼ A

Proof

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