Proof of Theorem mapfzcons
Step | Hyp | Ref
| Expression |
1 | | simp2 1135 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝐴 ∈ (𝐵 ↑m (1...𝑁))) |
2 | | elmapex 8610 |
. . . . . . . . 9
⊢ (𝐴 ∈ (𝐵 ↑m (1...𝑁)) → (𝐵 ∈ V ∧ (1...𝑁) ∈ V)) |
3 | 2 | simpld 494 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐵 ↑m (1...𝑁)) → 𝐵 ∈ V) |
4 | 3 | 3ad2ant2 1132 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝐵 ∈ V) |
5 | | ovex 7301 |
. . . . . . 7
⊢
(1...𝑁) ∈
V |
6 | | elmapg 8602 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ (1...𝑁) ∈ V) → (𝐴 ∈ (𝐵 ↑m (1...𝑁)) ↔ 𝐴:(1...𝑁)⟶𝐵)) |
7 | 4, 5, 6 | sylancl 585 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∈ (𝐵 ↑m (1...𝑁)) ↔ 𝐴:(1...𝑁)⟶𝐵)) |
8 | 1, 7 | mpbid 231 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝐴:(1...𝑁)⟶𝐵) |
9 | | ovex 7301 |
. . . . . . . 8
⊢ (𝑁 + 1) ∈ V |
10 | | simp3 1136 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
11 | | f1osng 6752 |
. . . . . . . 8
⊢ (((𝑁 + 1) ∈ V ∧ 𝐶 ∈ 𝐵) → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}–1-1-onto→{𝐶}) |
12 | 9, 10, 11 | sylancr 586 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}–1-1-onto→{𝐶}) |
13 | | f1of 6712 |
. . . . . . 7
⊢
({〈(𝑁 + 1),
𝐶〉}:{(𝑁 + 1)}–1-1-onto→{𝐶} → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶{𝐶}) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶{𝐶}) |
15 | | snssi 4746 |
. . . . . . 7
⊢ (𝐶 ∈ 𝐵 → {𝐶} ⊆ 𝐵) |
16 | 15 | 3ad2ant3 1133 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵) |
17 | 14, 16 | fssd 6614 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝐵) |
18 | | fzp1disj 13297 |
. . . . . 6
⊢
((1...𝑁) ∩
{(𝑁 + 1)}) =
∅ |
19 | 18 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅) |
20 | | fun 6632 |
. . . . 5
⊢ (((𝐴:(1...𝑁)⟶𝐵 ∧ {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝐵) ∧ ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅) → (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):((1...𝑁) ∪ {(𝑁 + 1)})⟶(𝐵 ∪ 𝐵)) |
21 | 8, 17, 19, 20 | syl21anc 834 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):((1...𝑁) ∪ {(𝑁 + 1)})⟶(𝐵 ∪ 𝐵)) |
22 | | 1z 12333 |
. . . . . . 7
⊢ 1 ∈
ℤ |
23 | | simp1 1134 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝑁 ∈
ℕ0) |
24 | | nn0uz 12602 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
25 | | 1m1e0 12028 |
. . . . . . . . . 10
⊢ (1
− 1) = 0 |
26 | 25 | fveq2i 6771 |
. . . . . . . . 9
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
27 | 24, 26 | eqtr4i 2770 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
28 | 23, 27 | eleqtrdi 2850 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝑁 ∈ (ℤ≥‘(1
− 1))) |
29 | | fzsuc2 13296 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ 𝑁
∈ (ℤ≥‘(1 − 1))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)})) |
30 | 22, 28, 29 | sylancr 586 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)})) |
31 | 30 | eqcomd 2745 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((1...𝑁) ∪ {(𝑁 + 1)}) = (1...(𝑁 + 1))) |
32 | | unidm 4090 |
. . . . . 6
⊢ (𝐵 ∪ 𝐵) = 𝐵 |
33 | 32 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐵 ∪ 𝐵) = 𝐵) |
34 | 31, 33 | feq23d 6591 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):((1...𝑁) ∪ {(𝑁 + 1)})⟶(𝐵 ∪ 𝐵) ↔ (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):(1...(𝑁 + 1))⟶𝐵)) |
35 | 21, 34 | mpbid 231 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):(1...(𝑁 + 1))⟶𝐵) |
36 | | ovex 7301 |
. . . 4
⊢
(1...(𝑁 + 1)) ∈
V |
37 | | elmapg 8602 |
. . . 4
⊢ ((𝐵 ∈ V ∧ (1...(𝑁 + 1)) ∈ V) → ((𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}) ∈ (𝐵 ↑m (1...(𝑁 + 1))) ↔ (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):(1...(𝑁 + 1))⟶𝐵)) |
38 | 4, 36, 37 | sylancl 585 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}) ∈ (𝐵 ↑m (1...(𝑁 + 1))) ↔ (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):(1...(𝑁 + 1))⟶𝐵)) |
39 | 35, 38 | mpbird 256 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}) ∈ (𝐵 ↑m (1...(𝑁 + 1)))) |
40 | | mapfzcons.1 |
. . . . 5
⊢ 𝑀 = (𝑁 + 1) |
41 | 40 | opeq1i 4812 |
. . . 4
⊢
〈𝑀, 𝐶〉 = 〈(𝑁 + 1), 𝐶〉 |
42 | 41 | sneqi 4577 |
. . 3
⊢
{〈𝑀, 𝐶〉} = {〈(𝑁 + 1), 𝐶〉} |
43 | 42 | uneq2i 4098 |
. 2
⊢ (𝐴 ∪ {〈𝑀, 𝐶〉}) = (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}) |
44 | 40 | oveq2i 7279 |
. . 3
⊢
(1...𝑀) =
(1...(𝑁 +
1)) |
45 | 44 | oveq2i 7279 |
. 2
⊢ (𝐵 ↑m (1...𝑀)) = (𝐵 ↑m (1...(𝑁 + 1))) |
46 | 39, 43, 45 | 3eltr4g 2857 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈𝑀, 𝐶〉}) ∈ (𝐵 ↑m (1...𝑀))) |