This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → ¬ 𝐵 < 𝐴 ) )