![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brsdom | Structured version Visualization version GIF version |
Description: Strict dominance relation, meaning "𝐵 is strictly greater in size than 𝐴". Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.) |
Ref | Expression |
---|---|
brsdom | ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sdom 8231 | . . 3 ⊢ ≺ = ( ≼ ∖ ≈ ) | |
2 | 1 | eleq2i 2898 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ ≺ ↔ 〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ )) |
3 | df-br 4876 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≺ ) | |
4 | df-br 4876 | . . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≼ ) | |
5 | df-br 4876 | . . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≈ ) | |
6 | 5 | notbii 312 | . . . 4 ⊢ (¬ 𝐴 ≈ 𝐵 ↔ ¬ 〈𝐴, 𝐵〉 ∈ ≈ ) |
7 | 4, 6 | anbi12i 620 | . . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ (〈𝐴, 𝐵〉 ∈ ≼ ∧ ¬ 〈𝐴, 𝐵〉 ∈ ≈ )) |
8 | eldif 3808 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ ) ↔ (〈𝐴, 𝐵〉 ∈ ≼ ∧ ¬ 〈𝐴, 𝐵〉 ∈ ≈ )) | |
9 | 7, 8 | bitr4i 270 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ 〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ )) |
10 | 2, 3, 9 | 3bitr4i 295 | 1 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 ∧ wa 386 ∈ wcel 2164 ∖ cdif 3795 〈cop 4405 class class class wbr 4875 ≈ cen 8225 ≼ cdom 8226 ≺ csdm 8227 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-dif 3801 df-br 4876 df-sdom 8231 |
This theorem is referenced by: sdomdom 8256 sdomnen 8257 0sdomg 8364 sdomdomtr 8368 domsdomtr 8370 domtriord 8381 canth2 8388 php2 8420 php3 8421 nnsdomo 8430 nnsdomg 8494 card2inf 8736 cardsdomelir 9119 cardsdom2 9134 fidomtri2 9140 cardmin2 9144 alephordi 9217 alephord 9218 isfin4-3 9459 isfin5-2 9535 canthnum 9793 canthwe 9795 canthp1 9798 gchcdaidm 9812 gchxpidm 9813 gchhar 9823 axgroth6 9972 hashsdom 13467 ruc 15353 |
Copyright terms: Public domain | W3C validator |