brsdom - Metamath Proof Explorer

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

Theorem brsdom 6852

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 6834	. . 3 $\$
2	1	eleq2i 2322	. 2 $\$
3		df-br 3998	. 2
4		df-br 3998	. . . 4
5		df-br 3998	. . . . 5
6	5	notbii 289	. . . 4
7	4, 6	anbi12i 681	. . 3 $/\$ $/\$
8		eldif 3137	. . 3 $\$ $/\$
9	7, 8	bitr4i 245	. 2 $/\$ $\$
10	2, 3, 9	3bitr4i 270	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 5

wb 178 $/\$ wa 360

wcel 1621 $\$ cdif 3124

cop 3617 class class class wbr 3997

cen 6828

cdom 6829

csdm 6830

This theorem is referenced by: sdomdom 6857 sdomnen 6858 0sdomg 6958 sdomdomtr 6962 domsdomtr 6964 domtriord 6975 canth2 6982 php2 7014 php3 7015 nnsdomo 7023 nnsdomg 7084 card2inf 7237 cardsdomelir 7574 cardsdom2 7589 fidomtri2 7595 cardmin2 7599 alephordi 7669 alephord 7670 isfin4-3 7909 isfin5-2 7985 canthnum 8239 canthwe 8241 canthp1 8244 gchcdaidm 8258 gchxpidm 8259 gchhar 8261 axgroth6 8418 hashsdom 11330 ruc 12484 carinttar 25270

This theorem was proved from axioms: ax-1 7 ax-2 8 ax-3 9 ax-mp 10 ax-5 1533 ax-6 1534 ax-7 1535 ax-gen 1536 ax-8 1623 ax-11 1624 ax-17 1628 ax-12o 1664 ax-10 1678 ax-9 1684 ax-4 1692 ax-16 1927 ax-ext 2239

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362 df-tru 1315 df-ex 1538 df-nf 1540 df-sb 1884 df-clab 2245 df-cleq 2251 df-clel 2254 df-nfc 2383 df-v 2765 df-dif 3130 df-br 3998 df-sdom 6834