| Step | Hyp | Ref
| Expression |
| 1 | | df-ne 2941 |
. . 3
⊢ ((𝐷 ∘ 𝑓) ≠ 0 ↔ ¬ (𝐷 ∘ 𝑓) = 0 ) |
| 2 | 1 | ralbii 3093 |
. 2
⊢
(∀𝑓 ∈
𝐵 (𝐷 ∘ 𝑓) ≠ 0 ↔ ∀𝑓 ∈ 𝐵 ¬ (𝐷 ∘ 𝑓) = 0 ) |
| 3 | | smndex2dbas.m |
. . . 4
⊢ 𝑀 =
(EndoFMnd‘ℕ0) |
| 4 | | smndex2dbas.b |
. . . 4
⊢ 𝐵 = (Base‘𝑀) |
| 5 | 3, 4 | efmndbasf 18888 |
. . 3
⊢ (𝑓 ∈ 𝐵 → 𝑓:ℕ0⟶ℕ0) |
| 6 | | 1nn0 12542 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
| 7 | | nn0z 12638 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℤ) |
| 8 | | 0zd 12625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℕ0
→ 0 ∈ ℤ) |
| 9 | | zneo 12701 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ 0 ∈
ℤ) → (2 · 𝑥) ≠ ((2 · 0) + 1)) |
| 10 | 7, 8, 9 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ (2 · 𝑥) ≠
((2 · 0) + 1)) |
| 11 | | 2t0e0 12435 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 0) = 0 |
| 12 | 11 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 0) + 1) = (0 + 1) |
| 13 | | 0p1e1 12388 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
| 14 | 12, 13 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· 0) + 1) = 1 |
| 15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℕ0
→ ((2 · 0) + 1) = 1) |
| 16 | 10, 15 | neeqtrd 3010 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℕ0
→ (2 · 𝑥) ≠
1) |
| 17 | 16 | necomd 2996 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℕ0
→ 1 ≠ (2 · 𝑥)) |
| 18 | 17 | neneqd 2945 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ0
→ ¬ 1 = (2 · 𝑥)) |
| 19 | 18 | nrex 3074 |
. . . . . . . . . . . 12
⊢ ¬
∃𝑥 ∈
ℕ0 1 = (2 · 𝑥) |
| 20 | | 1ex 11257 |
. . . . . . . . . . . . 13
⊢ 1 ∈
V |
| 21 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 1 → (𝑦 = (2 · 𝑥) ↔ 1 = (2 · 𝑥))) |
| 22 | 21 | rexbidv 3179 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 1 → (∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℕ0 1 =
(2 · 𝑥))) |
| 23 | 20, 22 | elab 3679 |
. . . . . . . . . . . 12
⊢ (1 ∈
{𝑦 ∣ ∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥)} ↔ ∃𝑥 ∈ ℕ0 1 =
(2 · 𝑥)) |
| 24 | 19, 23 | mtbir 323 |
. . . . . . . . . . 11
⊢ ¬ 1
∈ {𝑦 ∣
∃𝑥 ∈
ℕ0 𝑦 = (2
· 𝑥)} |
| 25 | | nelss 4049 |
. . . . . . . . . . 11
⊢ ((1
∈ ℕ0 ∧ ¬ 1 ∈ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)}) → ¬
ℕ0 ⊆ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)}) |
| 26 | 6, 24, 25 | mp2an 692 |
. . . . . . . . . 10
⊢ ¬
ℕ0 ⊆ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)} |
| 27 | 26 | intnan 486 |
. . . . . . . . 9
⊢ ¬
({𝑦 ∣ ∃𝑥 ∈ ℕ0
𝑦 = (2 · 𝑥)} ⊆ ℕ0
∧ ℕ0 ⊆ {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)}) |
| 28 | | eqss 3999 |
. . . . . . . . 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 5968 |
. . . . . . . . 9
⊢ ran 𝐷 = {𝑦 ∣ ∃𝑥 ∈ ℕ0 𝑦 = (2 · 𝑥)} |
| 32 | 31 | eqeq1i 2742 |
. . . . . . . 8
⊢ (ran
𝐷 = ℕ0
↔ {𝑦 ∣
∃𝑥 ∈
ℕ0 𝑦 = (2
· 𝑥)} =
ℕ0) |
| 33 | 29, 32 | mtbir 323 |
. . . . . . 7
⊢ ¬
ran 𝐷 =
ℕ0 |
| 34 | 33 | olci 867 |
. . . . . 6
⊢ (¬
𝐷 Fn ℕ0
∨ ¬ ran 𝐷 =
ℕ0) |
| 35 | | ianor 984 |
. . . . . . 7
⊢ (¬
(𝐷 Fn ℕ0
∧ ran 𝐷 =
ℕ0) ↔ (¬ 𝐷 Fn ℕ0 ∨ ¬ ran 𝐷 =
ℕ0)) |
| 36 | | df-fo 6567 |
. . . . . . 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 231 |
. . . . 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 18927 |
. . . . 5
⊢ 𝐷 ∈ 𝐵 |
| 42 | 3, 4 | efmndbasf 18888 |
. . . . 5
⊢ (𝐷 ∈ 𝐵 → 𝐷:ℕ0⟶ℕ0) |
| 43 | | simpl 482 |
. . . . . . 7
⊢ ((𝐷:ℕ0⟶ℕ0
∧ (𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 )) → 𝐷:ℕ0⟶ℕ0) |
| 44 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 ) → 𝑓:ℕ0⟶ℕ0) |
| 45 | 44 | adantl 481 |
. . . . . . 7
⊢ ((𝐷:ℕ0⟶ℕ0
∧ (𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 )) → 𝑓:ℕ0⟶ℕ0) |
| 46 | | nn0ex 12532 |
. . . . . . . . . . . . 13
⊢
ℕ0 ∈ V |
| 47 | 3 | efmndid 18901 |
. . . . . . . . . . . . 13
⊢
(ℕ0 ∈ V → ( I ↾ ℕ0) =
(0g‘𝑀)) |
| 48 | 46, 47 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ( I
↾ ℕ0) = (0g‘𝑀) |
| 49 | 40, 48 | eqtr4i 2768 |
. . . . . . . . . . 11
⊢ 0 = ( I ↾
ℕ0) |
| 50 | 49 | eqeq2i 2750 |
. . . . . . . . . 10
⊢ ((𝐷 ∘ 𝑓) = 0 ↔ (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) |
| 51 | 50 | biimpi 216 |
. . . . . . . . 9
⊢ ((𝐷 ∘ 𝑓) = 0 → (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) |
| 52 | 51 | adantl 481 |
. . . . . . . 8
⊢ ((𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 ) → (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) |
| 53 | 52 | adantl 481 |
. . . . . . 7
⊢ ((𝐷:ℕ0⟶ℕ0
∧ (𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 )) → (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) |
| 54 | | fcofo 7308 |
. . . . . . 7
⊢ ((𝐷:ℕ0⟶ℕ0
∧ 𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = ( I ↾
ℕ0)) → 𝐷:ℕ0–onto→ℕ0) |
| 55 | 43, 45, 53, 54 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐷:ℕ0⟶ℕ0
∧ (𝑓:ℕ0⟶ℕ0
∧ (𝐷 ∘ 𝑓) = 0 )) → 𝐷:ℕ0–onto→ℕ0) |
| 56 | 55 | ex 412 |
. . . . 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 816 |
. . 3
⊢ (𝑓:ℕ0⟶ℕ0
→ ¬ (𝐷 ∘ 𝑓) = 0 ) |
| 59 | 5, 58 | syl 17 |
. 2
⊢ (𝑓 ∈ 𝐵 → ¬ (𝐷 ∘ 𝑓) = 0 ) |
| 60 | 2, 59 | mprgbir 3068 |
1
⊢
∀𝑓 ∈
𝐵 (𝐷 ∘ 𝑓) ≠ 0 |