![]() |
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 8977 | . . 3 ⊢ ≺ = ( ≼ ∖ ≈ ) | |
2 | 1 | eleq2i 2818 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ ≺ ↔ 〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ )) |
3 | df-br 5154 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≺ ) | |
4 | df-br 5154 | . . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≼ ) | |
5 | df-br 5154 | . . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≈ ) | |
6 | 5 | notbii 319 | . . . 4 ⊢ (¬ 𝐴 ≈ 𝐵 ↔ ¬ 〈𝐴, 𝐵〉 ∈ ≈ ) |
7 | 4, 6 | anbi12i 626 | . . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ (〈𝐴, 𝐵〉 ∈ ≼ ∧ ¬ 〈𝐴, 𝐵〉 ∈ ≈ )) |
8 | eldif 3957 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ ) ↔ (〈𝐴, 𝐵〉 ∈ ≼ ∧ ¬ 〈𝐴, 𝐵〉 ∈ ≈ )) | |
9 | 7, 8 | bitr4i 277 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ 〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ )) |
10 | 2, 3, 9 | 3bitr4i 302 | 1 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 394 ∈ wcel 2099 ∖ cdif 3944 〈cop 4639 class class class wbr 5153 ≈ cen 8971 ≼ cdom 8972 ≺ csdm 8973 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-dif 3950 df-br 5154 df-sdom 8977 |
This theorem is referenced by: sdomdom 9011 sdomnen 9012 0sdomg 9142 0sdomgOLD 9143 sdom0 9146 sdomdomtr 9148 domsdomtr 9150 domtriord 9161 canth2 9168 sdomdomtrfi 9238 domsdomtrfi 9239 php2 9245 php2OLD 9257 php3OLD 9258 nnsdomo 9268 1sdom2 9274 sdom1 9276 1sdom2dom 9281 nnsdomg 9336 nnsdomgOLD 9337 card2inf 9598 cardsdomelir 10016 cardsdom2 10031 fidomtri2 10037 cardmin2 10042 alephordi 10117 alephord 10118 isfin4p1 10358 isfin5-2 10434 canthnum 10692 canthwe 10694 canthp1 10697 gchdjuidm 10711 gchxpidm 10712 gchhar 10722 axgroth6 10871 hashsdom 14398 ruc 16245 iscard5 43203 |
Copyright terms: Public domain | W3C validator |