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

Metamath Proof Explorer

Theorem nlt1pi

Description: No positive integer is less than one. (Contributed by NM, 23-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion nlt1pi ¬ 𝐴 <N 1o

Proof

Step Hyp Ref Expression
1 elni ⊢ ( 𝐴 ∈ N ↔ ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) )
2 1 simprbi ⊢ ( 𝐴 ∈ N → 𝐴 ≠ ∅ )
3 noel ⊢ ¬ 𝐴 ∈ ∅
4 1pi ⊢ 1o ∈ N
5 ltpiord ⊢ ( ( 𝐴 ∈ N ∧ 1o ∈ N ) → ( 𝐴 <N 1o ↔ 𝐴 ∈ 1o ) )
6 4 5 mpan2 ⊢ ( 𝐴 ∈ N → ( 𝐴 <N 1o ↔ 𝐴 ∈ 1o ) )
7 df-1o ⊢ 1o = suc ∅
8 7 eleq2i ⊢ ( 𝐴 ∈ 1o ↔ 𝐴 ∈ suc ∅ )
9 elsucg ⊢ ( 𝐴 ∈ N → ( 𝐴 ∈ suc ∅ ↔ ( 𝐴 ∈ ∅ ∨ 𝐴 = ∅ ) ) )
10 8 9 bitrid ⊢ ( 𝐴 ∈ N → ( 𝐴 ∈ 1o ↔ ( 𝐴 ∈ ∅ ∨ 𝐴 = ∅ ) ) )
11 6 10 bitrd ⊢ ( 𝐴 ∈ N → ( 𝐴 <N 1o ↔ ( 𝐴 ∈ ∅ ∨ 𝐴 = ∅ ) ) )
12 11 biimpa ⊢ ( ( 𝐴 ∈ N ∧ 𝐴 <N 1o ) → ( 𝐴 ∈ ∅ ∨ 𝐴 = ∅ ) )
13 12 ord ⊢ ( ( 𝐴 ∈ N ∧ 𝐴 <N 1o ) → ( ¬ 𝐴 ∈ ∅ → 𝐴 = ∅ ) )
14 3 13 mpi ⊢ ( ( 𝐴 ∈ N ∧ 𝐴 <N 1o ) → 𝐴 = ∅ )
15 14 ex ⊢ ( 𝐴 ∈ N → ( 𝐴 <N 1o → 𝐴 = ∅ ) )
16 15 necon3ad ⊢ ( 𝐴 ∈ N → ( 𝐴 ≠ ∅ → ¬ 𝐴 <N 1o ) )
17 2 16 mpd ⊢ ( 𝐴 ∈ N → ¬ 𝐴 <N 1o )
18 ltrelpi ⊢ <N ⊆ ( N × N )
19 18 brel ⊢ ( 𝐴 <N 1o → ( 𝐴 ∈ N ∧ 1o ∈ N ) )
20 19 simpld ⊢ ( 𝐴 <N 1o → 𝐴 ∈ N )
21 20 con3i ⊢ ( ¬ 𝐴 ∈ N → ¬ 𝐴 <N 1o )
22 17 21 pm2.61i ⊢ ¬ 𝐴 <N 1o