ltxr - Metamath Proof Explorer

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

Theorem ltxr 11320

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 4452	. . . . 5 $/\$
2		df-3an 975	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4511	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 5073	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 11	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4495	. . . 4 $\/$
7		brxp 5029	. . . . . . 7 $/\$
8		elun 3645	. . . . . . . . . . 11 $\/$
9		orcom 387	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 249	. . . . . . . . . 10 $\/$
11		elsncg 4050	. . . . . . . . . . 11
12	11	orbi1d 702	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	syl5bb 257	. . . . . . . . 9 $\/$
14		elsncg 4050	. . . . . . . . 9
15	13, 14	bi2anan9 871	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 866	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	syl6bb 261	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	syl5bb 257	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 5029	. . . . . . 7 $/\$
20	11	anbi1d 704	. . . . . . . 8 $/\$ $/\$
21	20	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
22	19, 21	syl5bb 257	. . . . . 6 $/\$ $/\$
23	18, 22	orbi12d 709	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		orass 524	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
25	23, 24	syl6bb 261	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	6, 25	syl5bb 257	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
27	5, 26	orbi12d 709	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
28		df-ltxr 9629	. . . 4 $/\$ $/\$
29	28	breqi 4453	. . 3 $/\$ $/\$
30		brun 4495	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
31	29, 30	bitri 249	. 2 $/\$ $/\$ $\/$
32		orass 524	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33	27, 31, 32	3bitr4g 288	1 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wcel 1767

cun 3474

csn 4027 class class class wbr 4447

copab 4504

cxp 4997

cr 9487

cltrr 9492

cpnf 9621

cmnf 9622

cxr 9623

clt 9624

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pr 4686

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-sn 4028 df-pr 4030 df-op 4034 df-br 4448 df-opab 4506 df-xp 5005 df-ltxr 9629

This theorem is referenced by: xrltnr 11326 ltpnf 11327 mnflt 11329 mnfltpnf 11331 pnfnlt 11333 nltmnf 11334

W3C validator