brsdom - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > brsdom		Unicode version

Theorem brsdom 7089

Description: Strict dominance relation, meaning "

is strictly greater in size than

." Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.)

**Assertion**
Ref	Expression
brsdom	$/\$

**Proof of Theorem brsdom**
Step	Hyp	Ref	Expression
1		df-sdom 7071	. . 3 $\$
2	1	eleq2i 2468	. 2 $\$
3		df-br 4173	. 2
4		df-br 4173	. . . 4
5		df-br 4173	. . . . 5
6	5	notbii 288	. . . 4
7	4, 6	anbi12i 679	. . 3 $/\$ $/\$
8		eldif 3290	. . 3 $\$ $/\$
9	7, 8	bitr4i 244	. 2 $/\$ $\$
10	2, 3, 9	3bitr4i 269	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wb 177 $/\$ wa 359

wcel 1721 $\$ cdif 3277

cop 3777 class class class wbr 4172

cen 7065

cdom 7066

csdm 7067

This theorem is referenced by: sdomdom 7094 sdomnen 7095 0sdomg 7195 sdomdomtr 7199 domsdomtr 7201 domtriord 7212 canth2 7219 php2 7251 php3 7252 nnsdomo 7260 nnsdomg 7325 card2inf 7479 cardsdomelir 7816 cardsdom2 7831 fidomtri2 7837 cardmin2 7841 alephordi 7911 alephord 7912 isfin4-3 8151 isfin5-2 8227 canthnum 8480 canthwe 8482 canthp1 8485 gchcdaidm 8499 gchxpidm 8500 gchhar 8502 axgroth6 8659 hashsdom 11610 ruc 12797

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385

This theorem depends on definitions: df-bi 178 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-v 2918 df-dif 3283 df-br 4173 df-sdom 7071