![]() |
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 8126 | . . 3 ⊢ ≺ = ( ≼ ∖ ≈ ) | |
2 | 1 | eleq2i 2831 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ ≺ ↔ 〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ )) |
3 | df-br 4805 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≺ ) | |
4 | df-br 4805 | . . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≼ ) | |
5 | df-br 4805 | . . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ≈ ) | |
6 | 5 | notbii 309 | . . . 4 ⊢ (¬ 𝐴 ≈ 𝐵 ↔ ¬ 〈𝐴, 𝐵〉 ∈ ≈ ) |
7 | 4, 6 | anbi12i 735 | . . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ (〈𝐴, 𝐵〉 ∈ ≼ ∧ ¬ 〈𝐴, 𝐵〉 ∈ ≈ )) |
8 | eldif 3725 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ ) ↔ (〈𝐴, 𝐵〉 ∈ ≼ ∧ ¬ 〈𝐴, 𝐵〉 ∈ ≈ )) | |
9 | 7, 8 | bitr4i 267 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ 〈𝐴, 𝐵〉 ∈ ( ≼ ∖ ≈ )) |
10 | 2, 3, 9 | 3bitr4i 292 | 1 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∧ wa 383 ∈ wcel 2139 ∖ cdif 3712 〈cop 4327 class class class wbr 4804 ≈ cen 8120 ≼ cdom 8121 ≺ csdm 8122 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-dif 3718 df-br 4805 df-sdom 8126 |
This theorem is referenced by: sdomdom 8151 sdomnen 8152 0sdomg 8256 sdomdomtr 8260 domsdomtr 8262 domtriord 8273 canth2 8280 php2 8312 php3 8313 nnsdomo 8322 nnsdomg 8386 card2inf 8627 cardsdomelir 9009 cardsdom2 9024 fidomtri2 9030 cardmin2 9034 alephordi 9107 alephord 9108 isfin4-3 9349 isfin5-2 9425 canthnum 9683 canthwe 9685 canthp1 9688 gchcdaidm 9702 gchxpidm 9703 gchhar 9713 axgroth6 9862 hashsdom 13382 ruc 15191 |
Copyright terms: Public domain | W3C validator |