Step | Hyp | Ref
| Expression |
1 | | elirrv 4509 |
. . . . . 6
⊢ ¬
𝑥 ∈ 𝑥 |
2 | | ltpiord 7241 |
. . . . . . 7
⊢ ((𝑥 ∈ N ∧
𝑥 ∈ N)
→ (𝑥
<N 𝑥 ↔ 𝑥 ∈ 𝑥)) |
3 | 2 | anidms 395 |
. . . . . 6
⊢ (𝑥 ∈ N →
(𝑥
<N 𝑥 ↔ 𝑥 ∈ 𝑥)) |
4 | 1, 3 | mtbiri 665 |
. . . . 5
⊢ (𝑥 ∈ N →
¬ 𝑥
<N 𝑥) |
5 | 4 | adantl 275 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ N) → ¬ 𝑥 <N 𝑥) |
6 | | pion 7232 |
. . . . . . . 8
⊢ (𝑧 ∈ N →
𝑧 ∈
On) |
7 | | ontr1 4351 |
. . . . . . . 8
⊢ (𝑧 ∈ On → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) |
8 | 6, 7 | syl 14 |
. . . . . . 7
⊢ (𝑧 ∈ N →
((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) |
9 | 8 | 3ad2ant3 1005 |
. . . . . 6
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N
∧ 𝑧 ∈
N) → ((𝑥
∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) |
10 | | ltpiord 7241 |
. . . . . . . 8
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ (𝑥
<N 𝑦 ↔ 𝑥 ∈ 𝑦)) |
11 | 10 | 3adant3 1002 |
. . . . . . 7
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N
∧ 𝑧 ∈
N) → (𝑥
<N 𝑦 ↔ 𝑥 ∈ 𝑦)) |
12 | | ltpiord 7241 |
. . . . . . . 8
⊢ ((𝑦 ∈ N ∧
𝑧 ∈ N)
→ (𝑦
<N 𝑧 ↔ 𝑦 ∈ 𝑧)) |
13 | 12 | 3adant1 1000 |
. . . . . . 7
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N
∧ 𝑧 ∈
N) → (𝑦
<N 𝑧 ↔ 𝑦 ∈ 𝑧)) |
14 | 11, 13 | anbi12d 465 |
. . . . . 6
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N
∧ 𝑧 ∈
N) → ((𝑥
<N 𝑦 ∧ 𝑦 <N 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧))) |
15 | | ltpiord 7241 |
. . . . . . 7
⊢ ((𝑥 ∈ N ∧
𝑧 ∈ N)
→ (𝑥
<N 𝑧 ↔ 𝑥 ∈ 𝑧)) |
16 | 15 | 3adant2 1001 |
. . . . . 6
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N
∧ 𝑧 ∈
N) → (𝑥
<N 𝑧 ↔ 𝑥 ∈ 𝑧)) |
17 | 9, 14, 16 | 3imtr4d 202 |
. . . . 5
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N
∧ 𝑧 ∈
N) → ((𝑥
<N 𝑦 ∧ 𝑦 <N 𝑧) → 𝑥 <N 𝑧)) |
18 | 17 | adantl 275 |
. . . 4
⊢
((⊤ ∧ (𝑥
∈ N ∧ 𝑦 ∈ N ∧ 𝑧 ∈ N)) →
((𝑥
<N 𝑦 ∧ 𝑦 <N 𝑧) → 𝑥 <N 𝑧)) |
19 | 5, 18 | ispod 4266 |
. . 3
⊢ (⊤
→ <N Po N) |
20 | | pinn 7231 |
. . . . . 6
⊢ (𝑥 ∈ N →
𝑥 ∈
ω) |
21 | | pinn 7231 |
. . . . . 6
⊢ (𝑦 ∈ N →
𝑦 ∈
ω) |
22 | | nntri3or 6442 |
. . . . . 6
⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
23 | 20, 21, 22 | syl2an 287 |
. . . . 5
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
24 | | biidd 171 |
. . . . . 6
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦)) |
25 | | ltpiord 7241 |
. . . . . . 7
⊢ ((𝑦 ∈ N ∧
𝑥 ∈ N)
→ (𝑦
<N 𝑥 ↔ 𝑦 ∈ 𝑥)) |
26 | 25 | ancoms 266 |
. . . . . 6
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ (𝑦
<N 𝑥 ↔ 𝑦 ∈ 𝑥)) |
27 | 10, 24, 26 | 3orbi123d 1293 |
. . . . 5
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ ((𝑥
<N 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 <N 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))) |
28 | 23, 27 | mpbird 166 |
. . . 4
⊢ ((𝑥 ∈ N ∧
𝑦 ∈ N)
→ (𝑥
<N 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 <N 𝑥)) |
29 | 28 | adantl 275 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ N ∧ 𝑦 ∈ N)) → (𝑥 <N
𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 <N 𝑥)) |
30 | 19, 29 | issod 4281 |
. 2
⊢ (⊤
→ <N Or N) |
31 | 30 | mptru 1344 |
1
⊢
<N Or N |