ltxr - Metamath Proof Explorer

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

Theorem ltxr 10671

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 4177	. . . . 5 $/\$
2		df-3an 938	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4232	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4910	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 11	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4218	. . . 4 $\/$
7		brxp 4868	. . . . . . 7 $/\$
8		elun 3448	. . . . . . . . . . 11 $\/$
9		orcom 377	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 241	. . . . . . . . . 10 $\/$
11		elsncg 3796	. . . . . . . . . . 11
12	11	orbi1d 684	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	syl5bb 249	. . . . . . . . 9 $\/$
14		elsncg 3796	. . . . . . . . 9
15	13, 14	bi2anan9 844	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 839	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	syl6bb 253	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	syl5bb 249	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 4868	. . . . . . 7 $/\$
20	11	anbi1d 686	. . . . . . . 8 $/\$ $/\$
21	20	adantr 452	. . . . . . 7 $/\$ $/\$ $/\$
22	19, 21	syl5bb 249	. . . . . 6 $/\$ $/\$
23	18, 22	orbi12d 691	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		orass 511	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
25	23, 24	syl6bb 253	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	6, 25	syl5bb 249	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
27	5, 26	orbi12d 691	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
28		df-ltxr 9081	. . . 4 $/\$ $/\$
29	28	breqi 4178	. . 3 $/\$ $/\$
30		brun 4218	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
31	29, 30	bitri 241	. 2 $/\$ $/\$ $\/$
32		orass 511	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33	27, 31, 32	3bitr4g 280	1 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

cun 3278

csn 3774 class class class wbr 4172

copab 4225

cxp 4835

cr 8945

cltrr 8950

cpnf 9073

cmnf 9074

cxr 9075

clt 9076

This theorem is referenced by: xrltnr 10676 ltpnf 10677 mnflt 10678 mnfltpnf 10679 pnfnlt 10681 nltmnf 10682

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pr 4363

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-rab 2675 df-v 2918 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-nul 3589 df-if 3700 df-sn 3780 df-pr 3781 df-op 3783 df-br 4173 df-opab 4227 df-xp 4843 df-ltxr 9081

W3C validator