ltxr - Metamath Proof Explorer

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

Theorem ltxr 11444

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 4421	. . . . 5 $/\$
2		df-3an 993	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4481	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4929	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 11	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4465	. . . 4 $\/$
7		brxp 4884	. . . . . . 7 $/\$
8		elun 3586	. . . . . . . . . . 11 $\/$
9		orcom 393	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 257	. . . . . . . . . 10 $\/$
11		elsncg 4003	. . . . . . . . . . 11
12	11	orbi1d 714	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	syl5bb 265	. . . . . . . . 9 $\/$
14		elsncg 4003	. . . . . . . . 9
15	13, 14	bi2anan9 889	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 884	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	syl6bb 269	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	syl5bb 265	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 4884	. . . . . . 7 $/\$
20	11	anbi1d 716	. . . . . . . 8 $/\$ $/\$
21	20	adantr 471	. . . . . . 7 $/\$ $/\$ $/\$
22	19, 21	syl5bb 265	. . . . . 6 $/\$ $/\$
23	18, 22	orbi12d 721	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		orass 531	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
25	23, 24	syl6bb 269	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	6, 25	syl5bb 265	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
27	5, 26	orbi12d 721	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
28		df-ltxr 9706	. . . 4 $/\$ $/\$
29	28	breqi 4422	. . 3 $/\$ $/\$
30		brun 4465	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
31	29, 30	bitri 257	. 2 $/\$ $/\$ $\/$
32		orass 531	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33	27, 31, 32	3bitr4g 296	1 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wcel 1898

cun 3414

csn 3980 class class class wbr 4416

copab 4474

cxp 4851

cr 9564

cltrr 9569

cpnf 9698

cmnf 9699

cxr 9700

clt 9701

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pr 4653

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-ral 2754 df-rex 2755 df-rab 2758 df-v 3059 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3744 df-if 3894 df-sn 3981 df-pr 3983 df-op 3987 df-br 4417 df-opab 4476 df-xp 4859 df-ltxr 9706

This theorem is referenced by: xrltnr 11450 ltpnf 11451 mnflt 11454 mnfltpnf 11457 pnfnlt 11459 nltmnf 11460

W3C validator