![]() |
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 8942 | . . 3 ⊢ ≺ = ( ≼ ∖ ≈ ) | |
2 | 1 | eleq2i 2826 | . 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ )) |
3 | df-br 5150 | . 2 ⊢ (𝐴 ≺ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ ) | |
4 | df-br 5150 | . . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ ) | |
5 | df-br 5150 | . . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ ) | |
6 | 5 | notbii 320 | . . . 4 ⊢ (¬ 𝐴 ≈ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ) |
7 | 4, 6 | anbi12i 628 | . . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )) |
8 | eldif 3959 | . . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )) | |
9 | 7, 8 | bitr4i 278 | . 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ )) |
10 | 2, 3, 9 | 3bitr4i 303 | 1 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 397 ∈ wcel 2107 ∖ cdif 3946 ⟨cop 4635 class class class wbr 5149 ≈ cen 8936 ≼ cdom 8937 ≺ csdm 8938 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-dif 3952 df-br 5150 df-sdom 8942 |
This theorem is referenced by: sdomdom 8976 sdomnen 8977 0sdomg 9104 0sdomgOLD 9105 sdom0 9108 sdomdomtr 9110 domsdomtr 9112 domtriord 9123 canth2 9130 sdomdomtrfi 9204 domsdomtrfi 9205 php2 9211 php2OLD 9223 php3OLD 9224 nnsdomo 9234 1sdom2 9240 sdom1 9242 1sdom2dom 9247 nnsdomg 9302 nnsdomgOLD 9303 card2inf 9550 cardsdomelir 9968 cardsdom2 9983 fidomtri2 9989 cardmin2 9994 alephordi 10069 alephord 10070 isfin4p1 10310 isfin5-2 10386 canthnum 10644 canthwe 10646 canthp1 10649 gchdjuidm 10663 gchxpidm 10664 gchhar 10674 axgroth6 10823 hashsdom 14341 ruc 16186 iscard5 42287 |
Copyright terms: Public domain | W3C validator |