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

Metamath Proof Explorer

Theorem brsdom

Description: Strict dominance relation, meaning " B is strictly greater in size than A ". Definition of Mendelson p. 255. (Contributed by NM, 25-Jun-1998)

Ref Expression
Assertion brsdom ⊢ A ≺ B ↔ A ≼ B ∧ ¬ A ≈ B

Proof

Step Hyp Ref Expression
1 df-sdom ⊢ ≺ = ≼ ∖ ≈
2 1 eleq2i ⊢ A B ∈ ≺ ↔ A B ∈ ≼ ∖ ≈
3 df-br ⊢ A ≺ B ↔ A B ∈ ≺
4 df-br ⊢ A ≼ B ↔ A B ∈ ≼
5 df-br ⊢ A ≈ B ↔ A B ∈ ≈
6 5 notbii ⊢ ¬ A ≈ B ↔ ¬ A B ∈ ≈
7 4 6 anbi12i ⊢ A ≼ B ∧ ¬ A ≈ B ↔ A B ∈ ≼ ∧ ¬ A B ∈ ≈
8 eldif ⊢ A B ∈ ≼ ∖ ≈ ↔ A B ∈ ≼ ∧ ¬ A B ∈ ≈
9 7 8 bitr4i ⊢ A ≼ B ∧ ¬ A ≈ B ↔ A B ∈ ≼ ∖ ≈
10 2 3 9 3bitr4i ⊢ A ≺ B ↔ A ≼ B ∧ ¬ A ≈ B