ltxr - Metamath Proof Explorer

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

Theorem ltxr 11349

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 4461	. . . . 5 $/\$
2		df-3an 975	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4521	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 5084	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 11	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4504	. . . 4 $\/$
7		brxp 5039	. . . . . . 7 $/\$
8		elun 3641	. . . . . . . . . . 11 $\/$
9		orcom 387	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 249	. . . . . . . . . 10 $\/$
11		elsncg 4055	. . . . . . . . . . 11
12	11	orbi1d 702	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	syl5bb 257	. . . . . . . . 9 $\/$
14		elsncg 4055	. . . . . . . . 9
15	13, 14	bi2anan9 873	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 868	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	syl6bb 261	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	syl5bb 257	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 5039	. . . . . . 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 9650	. . . 4 $/\$ $/\$
29	28	breqi 4462	. . 3 $/\$ $/\$
30		brun 4504	. . 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 1395

wcel 1819

cun 3469

csn 4032 class class class wbr 4456

copab 4514

cxp 5006

cr 9508

cltrr 9513

cpnf 9642

cmnf 9643

cxr 9644

clt 9645

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pr 4695

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-sn 4033 df-pr 4035 df-op 4039 df-br 4457 df-opab 4516 df-xp 5014 df-ltxr 9650

This theorem is referenced by: xrltnr 11355 ltpnf 11356 mnflt 11358 mnfltpnf 11360 pnfnlt 11362 nltmnf 11363

W3C validator