ltxr - Metamath Proof Explorer

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

Theorem ltxr 11404

Description: The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 14-Oct-2005.)

**Assertion**
Ref	Expression
ltxr	$/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Proof of Theorem ltxr Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq12 4422	. . . . 5 $/\$
2		df-3an 984	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4481	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4921	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 11	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4465	. . . 4 $\/$
7		brxp 4876	. . . . . . 7 $/\$
8		elun 3603	. . . . . . . . . . 11 $\/$
9		orcom 388	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 252	. . . . . . . . . 10 $\/$
11		elsncg 4016	. . . . . . . . . . 11
12	11	orbi1d 707	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	syl5bb 260	. . . . . . . . 9 $\/$
14		elsncg 4016	. . . . . . . . 9
15	13, 14	bi2anan9 881	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 876	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	syl6bb 264	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	syl5bb 260	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 4876	. . . . . . 7 $/\$
20	11	anbi1d 709	. . . . . . . 8 $/\$ $/\$
21	20	adantr 466	. . . . . . 7 $/\$ $/\$ $/\$
22	19, 21	syl5bb 260	. . . . . 6 $/\$ $/\$
23	18, 22	orbi12d 714	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		orass 526	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
25	23, 24	syl6bb 264	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	6, 25	syl5bb 260	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
27	5, 26	orbi12d 714	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
28		df-ltxr 9669	. . . 4 $/\$ $/\$
29	28	breqi 4423	. . 3 $/\$ $/\$
30		brun 4465	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
31	29, 30	bitri 252	. 2 $/\$ $/\$ $\/$
32		orass 526	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33	27, 31, 32	3bitr4g 291	1 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867

cun 3431

csn 3993 class class class wbr 4417

copab 4474

cxp 4843

cr 9527

cltrr 9532

cpnf 9661

cmnf 9662

cxr 9663

clt 9664

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-sep 4539 ax-nul 4547 ax-pr 4652

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-ral 2778 df-rex 2779 df-rab 2782 df-v 3080 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-nul 3759 df-if 3907 df-sn 3994 df-pr 3996 df-op 4000 df-br 4418 df-opab 4476 df-xp 4851 df-ltxr 9669

This theorem is referenced by: xrltnr 11410 ltpnf 11411 mnflt 11414 mnfltpnf 11417 pnfnlt 11419 nltmnf 11420

W3C validator