brsdom - Metamath Proof Explorer

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

Theorem brsdom 7122

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 7104	. . 3 $\$
2	1	eleq2i 2499	. 2 $\$
3		df-br 4205	. 2
4		df-br 4205	. . . 4
5		df-br 4205	. . . . 5
6	5	notbii 288	. . . 4
7	4, 6	anbi12i 679	. . 3 $/\$ $/\$
8		eldif 3322	. . 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 1725 $\$ cdif 3309

cop 3809 class class class wbr 4204

cen 7098

cdom 7099

csdm 7100

This theorem is referenced by: sdomdom 7127 sdomnen 7128 0sdomg 7228 sdomdomtr 7232 domsdomtr 7234 domtriord 7245 canth2 7252 php2 7284 php3 7285 nnsdomo 7293 nnsdomg 7358 card2inf 7515 cardsdomelir 7852 cardsdom2 7867 fidomtri2 7873 cardmin2 7877 alephordi 7947 alephord 7948 isfin4-3 8187 isfin5-2 8263 canthnum 8516 canthwe 8518 canthp1 8521 gchcdaidm 8535 gchxpidm 8536 gchhar 8538 axgroth6 8695 hashsdom 11647 ruc 12834

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1555 ax-5 1566 ax-17 1626 ax-9 1666 ax-8 1687 ax-6 1744 ax-7 1749 ax-11 1761 ax-12 1950 ax-ext 2416

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-tru 1328 df-ex 1551 df-nf 1554 df-sb 1659 df-clab 2422 df-cleq 2428 df-clel 2431 df-nfc 2560 df-v 2950 df-dif 3315 df-br 4205 df-sdom 7104