Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > brdom2 | Structured version Visualization version GIF version |
Description: Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97. (Contributed by NM, 17-Jun-1998.) |
Ref | Expression |
---|---|
brdom2 | ⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfdom2 8766 | . . 3 ⊢ ≼ = ( ≺ ∪ ≈ ) | |
2 | 1 | eleq2i 2830 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ ≼ ↔ 〈𝐴, 𝐵〉 ∈ ( ≺ ∪ ≈ )) |
3 | df-br 5075 | . 2 ⊢ (𝐴 ≼ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≼ ) | |
4 | df-br 5075 | . . . 4 ⊢ (𝐴 ≺ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≺ ) | |
5 | df-br 5075 | . . . 4 ⊢ (𝐴 ≈ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≈ ) | |
6 | 4, 5 | orbi12i 912 | . . 3 ⊢ ((𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵) ↔ (〈𝐴, 𝐵〉 ∈ ≺ ∨ 〈𝐴, 𝐵〉 ∈ ≈ )) |
7 | elun 4083 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ ( ≺ ∪ ≈ ) ↔ (〈𝐴, 𝐵〉 ∈ ≺ ∨ 〈𝐴, 𝐵〉 ∈ ≈ )) | |
8 | 6, 7 | bitr4i 277 | . 2 ⊢ ((𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵) ↔ 〈𝐴, 𝐵〉 ∈ ( ≺ ∪ ≈ )) |
9 | 2, 3, 8 | 3bitr4i 303 | 1 ⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 844 ∈ wcel 2106 ∪ cun 3885 〈cop 4567 class class class wbr 5074 ≈ cen 8730 ≼ cdom 8731 ≺ csdm 8732 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-xp 5595 df-rel 5596 df-f1o 6440 df-en 8734 df-dom 8735 df-sdom 8736 |
This theorem is referenced by: bren2 8771 domnsym 8886 domnsymfi 8986 modom 9023 carddom2 9735 axcc4dom 10197 entric 10313 entri2 10314 gchor 10383 frgpcyg 20781 iunmbl2 24721 dyadmbl 24764 padct 31054 volmeas 32199 ovoliunnfl 35819 ctbnfien 40640 |
Copyright terms: Public domain | W3C validator |