Step | Hyp | Ref
| Expression |
1 | | df-ne 2944 |
. . 3
⊢ ((𝐷 ∘ 𝑓) ≠ 0 ↔ ¬ (𝐷 ∘ 𝑓) = 0 ) |
2 | 1 | ralbii 3092 |
. 2
⊢
(∀𝑓 ∈
𝐵 (𝐷 ∘ 𝑓) ≠ 0 ↔ ∀𝑓 ∈ 𝐵 ¬ (𝐷 ∘ 𝑓) = 0 ) |
3 | | smndex2dbas.m |
. . . 4
⊢ 𝑀 =
(EndoFMnd‘ℕ0) |
4 | | smndex2dbas.b |
. . . 4
⊢ 𝐵 = (Base‘𝑀) |
5 | 3, 4 | efmndbasf 18514 |
. . 3
⊢ (𝑓 ∈ 𝐵 → 𝑓:ℕ0⟶ℕ0) |
6 | | 1nn0 12249 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
7 | | nn0z 12343 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℤ) |
8 | | 0zd 12331 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ 0 ∈ ℤ) |
9 | | zneo 12403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 0 ∈
ℤ) → (2 · 𝑥) ≠ ((2 · 0) + 1)) |
10 | 7, 8, 9 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (2 · 𝑥) ≠
((2 · 0) + 1)) |
11 | | 2t0e0 12142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 0) = 0 |
12 | 11 | oveq1i 7285 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 0) + 1) = (0 + 1) |
13 | | 0p1e1 12095 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
14 | 12, 13 | eqtri 2766 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· 0) + 1) = 1 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ ((2 · 0) + 1) = 1) |
16 | 10, 15 | neeqtrd 3013 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
→ (2 · 𝑥) ≠
1) |
17 | 16 | necomd 2999 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ0
→ 1 ≠ (2 · 𝑥)) |
18 | 17 | neneqd 2948 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ0
→ ¬ 1 = (2 · 𝑥)) |
19 | 18 | nrex 3197 |
. . . . . . . . . . . 12
⊢ ¬
∃𝑥 ∈
ℕ0 1 = (2 · 𝑥) |
20 | | 1ex 10971 |
. . . . . . . . . . . . 13
⊢ 1 ∈
V |
21 | | eqeq1 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 1 → (𝑦 = (2 · 𝑥) ↔ 1 = (2 · 𝑥))) |
22 | 21 | rexbidv 3226 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 1 → (∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℕ0 1 =
(2 · 𝑥))) |
23 | 20, 22 | elab 3609 |
. . . . . . . . . . . 12
⊢ (1 ∈
{𝑦 ∣ ∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥)} ↔ ∃𝑥 ∈ ℕ0 1 =
(2 · 𝑥)) |
24 | 19, 23 | mtbir 323 |
. . . . . . . . . . 11
⊢ ¬ 1
∈ {𝑦 ∣
∃𝑥 ∈
ℕ0 𝑦 = (2
· 𝑥)} |
25 | | nelss 3984 |
. . . . . . . . . . 11
⊢ ((1
∈ ℕ0 ∧ ¬ 1 ∈ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)}) → ¬
ℕ0 ⊆ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)}) |
26 | 6, 24, 25 | mp2an 689 |
. . . . . . . . . 10
⊢ ¬
ℕ0 ⊆ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)} |
27 | 26 | intnan 487 |
. . . . . . . . 9
⊢ ¬
({𝑦 ∣ ∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥)} ⊆ ℕ0
∧ ℕ0 ⊆ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)}) |
28 | | eqss 3936 |
. . . . . . . . 9
⊢ ({𝑦 ∣ ∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥)} = ℕ0 ↔
({𝑦 ∣ ∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥)} ⊆ ℕ0
∧ ℕ0 ⊆ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)})) |
29 | 27, 28 | mtbir 323 |
. . . . . . . 8
⊢ ¬
{𝑦 ∣ ∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥)} =
ℕ0 |
30 | | smndex2dbas.d |
. . . . . . . . . 10
⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2
· 𝑥)) |
31 | 30 | rnmpt 5864 |
. . . . . . . . 9
⊢ ran 𝐷 = {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)} |
32 | 31 | eqeq1i 2743 |
. . . . . . . 8
⊢ (ran
𝐷 = ℕ0
↔ {𝑦 ∣
∃𝑥 ∈
ℕ0 𝑦 = (2
· 𝑥)} =
ℕ0) |
33 | 29, 32 | mtbir 323 |
. . . . . . 7
⊢ ¬
ran 𝐷 =
ℕ0 |
34 | 33 | olci 863 |
. . . . . 6
⊢ (¬
𝐷 Fn ℕ0
∨ ¬ ran 𝐷 =
ℕ0) |
35 | | ianor 979 |
. . . . . . 7
⊢ (¬
(𝐷 Fn ℕ0
∧ ran 𝐷 =
ℕ0) ↔ (¬ 𝐷 Fn ℕ0 ∨ ¬ ran 𝐷 =
ℕ0)) |
36 | | df-fo 6439 |
. . . . . . 7
⊢ (𝐷:ℕ0–onto→ℕ0 ↔ (𝐷 Fn ℕ0 ∧
ran 𝐷 =
ℕ0)) |
37 | 35, 36 | xchnxbir 333 |
. . . . . 6
⊢ (¬
𝐷:ℕ0–onto→ℕ0 ↔ (¬ 𝐷 Fn ℕ0 ∨
¬ ran 𝐷 =
ℕ0)) |
38 | 34, 37 | mpbir 230 |
. . . . 5
⊢ ¬
𝐷:ℕ0–onto→ℕ0 |
39 | 38 | a1i 11 |
. . . 4
⊢ (𝑓:ℕ0⟶ℕ0
→ ¬ 𝐷:ℕ0–onto→ℕ0) |
40 | | smndex2dbas.0 |
. . . . . 6
⊢ 0 =
(0g‘𝑀) |
41 | 3, 4, 40, 30 | smndex2dbas 18553 |
. . . . 5
⊢ 𝐷 ∈ 𝐵 |
42 | 3, 4 | efmndbasf 18514 |
. . . . 5
⊢ (𝐷 ∈ 𝐵 → 𝐷:ℕ0⟶ℕ0) |
43 | | simpl 483 |
. . . . . . 7
⊢ ((𝐷:ℕ0⟶ℕ0
∧ (𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 )) → 𝐷:ℕ0⟶ℕ0) |
44 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 ) → 𝑓:ℕ0⟶ℕ0) |
45 | 44 | adantl 482 |
. . . . . . 7
⊢ ((𝐷:ℕ0⟶ℕ0
∧ (𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 )) → 𝑓:ℕ0⟶ℕ0) |
46 | | nn0ex 12239 |
. . . . . . . . . . . . 13
⊢
ℕ0 ∈ V |
47 | 3 | efmndid 18527 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ∈ V → ( I ↾ ℕ0) =
(0g‘𝑀)) |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ( I
↾ ℕ0) = (0g‘𝑀) |
49 | 40, 48 | eqtr4i 2769 |
. . . . . . . . . . 11
⊢ 0 = ( I ↾
ℕ0) |
50 | 49 | eqeq2i 2751 |
. . . . . . . . . 10
⊢ ((𝐷 ∘ 𝑓) = 0 ↔ (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) |
51 | 50 | biimpi 215 |
. . . . . . . . 9
⊢ ((𝐷 ∘ 𝑓) = 0 → (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) |
52 | 51 | adantl 482 |
. . . . . . . 8
⊢ ((𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 ) → (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) |
53 | 52 | adantl 482 |
. . . . . . 7
⊢ ((𝐷:ℕ0⟶ℕ0
∧ (𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 )) → (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) |
54 | | fcofo 7160 |
. . . . . . 7
⊢ ((𝐷:ℕ0⟶ℕ0
∧ 𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) → 𝐷:ℕ0–onto→ℕ0) |
55 | 43, 45, 53, 54 | syl3anc 1370 |
. . . . . 6
⊢ ((𝐷:ℕ0⟶ℕ0
∧ (𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 )) → 𝐷:ℕ0–onto→ℕ0) |
56 | 55 | ex 413 |
. . . . 5
⊢ (𝐷:ℕ0⟶ℕ0
→ ((𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 ) → 𝐷:ℕ0–onto→ℕ0)) |
57 | 41, 42, 56 | mp2b 10 |
. . . 4
⊢ ((𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 ) → 𝐷:ℕ0–onto→ℕ0) |
58 | 39, 57 | mtand 813 |
. . 3
⊢ (𝑓:ℕ0⟶ℕ0
→ ¬ (𝐷 ∘ 𝑓) = 0 ) |
59 | 5, 58 | syl 17 |
. 2
⊢ (𝑓 ∈ 𝐵 → ¬ (𝐷 ∘ 𝑓) = 0 ) |
60 | 2, 59 | mprgbir 3079 |
1
⊢
∀𝑓 ∈
𝐵 (𝐷 ∘ 𝑓) ≠ 0 |