Theorem xrltnsym

Description: Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005)

	Ref	Expression
Assertion	xrltnsym	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2		elxr	⊢ ( 𝐵 ∈ ℝ* ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) )
3		ltnsym	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
4		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
5		pnfnlt	⊢ ( 𝐴 ∈ ℝ* → ¬ +∞ < 𝐴 )
6	4 5	syl	⊢ ( 𝐴 ∈ ℝ → ¬ +∞ < 𝐴 )
7	6	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ¬ +∞ < 𝐴 )
8		breq1	⊢ ( 𝐵 = +∞ → ( 𝐵 < 𝐴 ↔ +∞ < 𝐴 ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐵 < 𝐴 ↔ +∞ < 𝐴 ) )
10	7 9	mtbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ¬ 𝐵 < 𝐴 )
11	10	a1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
12		nltmnf	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < -∞ )
13	4 12	syl	⊢ ( 𝐴 ∈ ℝ → ¬ 𝐴 < -∞ )
14	13	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ¬ 𝐴 < -∞ )
15		breq2	⊢ ( 𝐵 = -∞ → ( 𝐴 < 𝐵 ↔ 𝐴 < -∞ ) )
16	15	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 ↔ 𝐴 < -∞ ) )
17	14 16	mtbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ¬ 𝐴 < 𝐵 )
18	17	pm2.21d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
19	3 11 18	3jaodan	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
20		pnfnlt	⊢ ( 𝐵 ∈ ℝ* → ¬ +∞ < 𝐵 )
21	20	adantl	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ¬ +∞ < 𝐵 )
22		breq1	⊢ ( 𝐴 = +∞ → ( 𝐴 < 𝐵 ↔ +∞ < 𝐵 ) )
23	22	adantr	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ +∞ < 𝐵 ) )
24	21 23	mtbird	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ¬ 𝐴 < 𝐵 )
25	24	pm2.21d	⊢ ( ( 𝐴 = +∞ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
26	2 25	sylan2br	⊢ ( ( 𝐴 = +∞ ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
27		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
28		nltmnf	⊢ ( 𝐵 ∈ ℝ* → ¬ 𝐵 < -∞ )
29	27 28	syl	⊢ ( 𝐵 ∈ ℝ → ¬ 𝐵 < -∞ )
30	29	adantl	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ¬ 𝐵 < -∞ )
31		breq2	⊢ ( 𝐴 = -∞ → ( 𝐵 < 𝐴 ↔ 𝐵 < -∞ ) )
32	31	adantr	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ 𝐵 < -∞ ) )
33	30 32	mtbird	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ¬ 𝐵 < 𝐴 )
34	33	a1d	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
35		mnfxr	⊢ -∞ ∈ ℝ*
36		pnfnlt	⊢ ( -∞ ∈ ℝ* → ¬ +∞ < -∞ )
37	35 36	ax-mp	⊢ ¬ +∞ < -∞
38		breq12	⊢ ( ( 𝐵 = +∞ ∧ 𝐴 = -∞ ) → ( 𝐵 < 𝐴 ↔ +∞ < -∞ ) )
39	37 38	mtbiri	⊢ ( ( 𝐵 = +∞ ∧ 𝐴 = -∞ ) → ¬ 𝐵 < 𝐴 )
40	39	ancoms	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) → ¬ 𝐵 < 𝐴 )
41	40	a1d	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
42		xrltnr	⊢ ( -∞ ∈ ℝ* → ¬ -∞ < -∞ )
43	35 42	ax-mp	⊢ ¬ -∞ < -∞
44		breq12	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 ↔ -∞ < -∞ ) )
45	43 44	mtbiri	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 = -∞ ) → ¬ 𝐴 < 𝐵 )
46	45	pm2.21d	⊢ ( ( 𝐴 = -∞ ∧ 𝐵 = -∞ ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
47	34 41 46	3jaodan	⊢ ( ( 𝐴 = -∞ ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
48	19 26 47	3jaoian	⊢ ( ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ∧ ( 𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞ ) ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )
49	1 2 48	syl2anb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )