Description: Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of Suppes p. 97. (Contributed by NM, 17-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | brdom2 | ⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfdom2 | ⊢ ≼ = ( ≺ ∪ ≈ ) | |
2 | 1 | eleq2i | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≺ ∪ ≈ ) ) |
3 | df-br | ⊢ ( 𝐴 ≼ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ ) | |
4 | df-br | ⊢ ( 𝐴 ≺ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ ) | |
5 | df-br | ⊢ ( 𝐴 ≈ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≈ ) | |
6 | 4 5 | orbi12i | ⊢ ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ ∨ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≈ ) ) |
7 | elun | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≺ ∪ ≈ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ ∨ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≈ ) ) | |
8 | 6 7 | bitr4i | ⊢ ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≺ ∪ ≈ ) ) |
9 | 2 3 8 | 3bitr4i | ⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ) |