ltxr - Metamath Proof Explorer

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

Theorem ltxr 11114

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 4316	. . . . 5 $/\$
2		df-3an 967	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4375	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4931	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 11	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4359	. . . 4 $\/$
7		brxp 4889	. . . . . . 7 $/\$
8		elun 3516	. . . . . . . . . . 11 $\/$
9		orcom 387	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 249	. . . . . . . . . 10 $\/$
11		elsncg 3919	. . . . . . . . . . 11
12	11	orbi1d 702	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	syl5bb 257	. . . . . . . . 9 $\/$
14		elsncg 3919	. . . . . . . . 9
15	13, 14	bi2anan9 868	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 863	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	syl6bb 261	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	syl5bb 257	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 4889	. . . . . . 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 9442	. . . 4 $/\$ $/\$
29	28	breqi 4317	. . 3 $/\$ $/\$
30		brun 4359	. . 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 965

wceq 1369

wcel 1756

cun 3345

csn 3896 class class class wbr 4311

copab 4368

cxp 4857

cr 9300

cltrr 9305

cpnf 9434

cmnf 9435

cxr 9436

clt 9437

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4432 ax-nul 4440 ax-pr 4550

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-ral 2739 df-rex 2740 df-rab 2743 df-v 2993 df-dif 3350 df-un 3352 df-in 3354 df-ss 3361 df-nul 3657 df-if 3811 df-sn 3897 df-pr 3899 df-op 3903 df-br 4312 df-opab 4370 df-xp 4865 df-ltxr 9442

This theorem is referenced by: xrltnr 11120 ltpnf 11121 mnflt 11123 mnfltpnf 11125 pnfnlt 11127 nltmnf 11128

W3C validator