Proof of Theorem mapfzcons
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp2 1138 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝐴 ∈ (𝐵 ↑m (1...𝑁))) | 
| 2 |  | elmapex 8888 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝐵 ↑m (1...𝑁)) → (𝐵 ∈ V ∧ (1...𝑁) ∈ V)) | 
| 3 | 2 | simpld 494 | . . . . . . . 8
⊢ (𝐴 ∈ (𝐵 ↑m (1...𝑁)) → 𝐵 ∈ V) | 
| 4 | 3 | 3ad2ant2 1135 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝐵 ∈ V) | 
| 5 |  | ovex 7464 | . . . . . . 7
⊢
(1...𝑁) ∈
V | 
| 6 |  | elmapg 8879 | . . . . . . 7
⊢ ((𝐵 ∈ V ∧ (1...𝑁) ∈ V) → (𝐴 ∈ (𝐵 ↑m (1...𝑁)) ↔ 𝐴:(1...𝑁)⟶𝐵)) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∈ (𝐵 ↑m (1...𝑁)) ↔ 𝐴:(1...𝑁)⟶𝐵)) | 
| 8 | 1, 7 | mpbid 232 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝐴:(1...𝑁)⟶𝐵) | 
| 9 |  | ovex 7464 | . . . . . . . 8
⊢ (𝑁 + 1) ∈ V | 
| 10 |  | simp3 1139 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) | 
| 11 |  | f1osng 6889 | . . . . . . . 8
⊢ (((𝑁 + 1) ∈ V ∧ 𝐶 ∈ 𝐵) → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}–1-1-onto→{𝐶}) | 
| 12 | 9, 10, 11 | sylancr 587 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}–1-1-onto→{𝐶}) | 
| 13 |  | f1of 6848 | . . . . . . 7
⊢
({〈(𝑁 + 1),
𝐶〉}:{(𝑁 + 1)}–1-1-onto→{𝐶} → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶{𝐶}) | 
| 14 | 12, 13 | syl 17 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶{𝐶}) | 
| 15 |  | snssi 4808 | . . . . . . 7
⊢ (𝐶 ∈ 𝐵 → {𝐶} ⊆ 𝐵) | 
| 16 | 15 | 3ad2ant3 1136 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵) | 
| 17 | 14, 16 | fssd 6753 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝐵) | 
| 18 |  | fzp1disj 13623 | . . . . . 6
⊢
((1...𝑁) ∩
{(𝑁 + 1)}) =
∅ | 
| 19 | 18 | a1i 11 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅) | 
| 20 |  | fun 6770 | . . . . 5
⊢ (((𝐴:(1...𝑁)⟶𝐵 ∧ {〈(𝑁 + 1), 𝐶〉}:{(𝑁 + 1)}⟶𝐵) ∧ ((1...𝑁) ∩ {(𝑁 + 1)}) = ∅) → (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):((1...𝑁) ∪ {(𝑁 + 1)})⟶(𝐵 ∪ 𝐵)) | 
| 21 | 8, 17, 19, 20 | syl21anc 838 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):((1...𝑁) ∪ {(𝑁 + 1)})⟶(𝐵 ∪ 𝐵)) | 
| 22 |  | 1z 12647 | . . . . . . 7
⊢ 1 ∈
ℤ | 
| 23 |  | simp1 1137 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝑁 ∈
ℕ0) | 
| 24 |  | nn0uz 12920 | . . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) | 
| 25 |  | 1m1e0 12338 | . . . . . . . . . 10
⊢ (1
− 1) = 0 | 
| 26 | 25 | fveq2i 6909 | . . . . . . . . 9
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) | 
| 27 | 24, 26 | eqtr4i 2768 | . . . . . . . 8
⊢
ℕ0 = (ℤ≥‘(1 −
1)) | 
| 28 | 23, 27 | eleqtrdi 2851 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → 𝑁 ∈ (ℤ≥‘(1
− 1))) | 
| 29 |  | fzsuc2 13622 | . . . . . . 7
⊢ ((1
∈ ℤ ∧ 𝑁
∈ (ℤ≥‘(1 − 1))) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)})) | 
| 30 | 22, 28, 29 | sylancr 587 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (1...(𝑁 + 1)) = ((1...𝑁) ∪ {(𝑁 + 1)})) | 
| 31 | 30 | eqcomd 2743 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((1...𝑁) ∪ {(𝑁 + 1)}) = (1...(𝑁 + 1))) | 
| 32 |  | unidm 4157 | . . . . . 6
⊢ (𝐵 ∪ 𝐵) = 𝐵 | 
| 33 | 32 | a1i 11 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐵 ∪ 𝐵) = 𝐵) | 
| 34 | 31, 33 | feq23d 6731 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):((1...𝑁) ∪ {(𝑁 + 1)})⟶(𝐵 ∪ 𝐵) ↔ (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):(1...(𝑁 + 1))⟶𝐵)) | 
| 35 | 21, 34 | mpbid 232 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):(1...(𝑁 + 1))⟶𝐵) | 
| 36 |  | ovex 7464 | . . . 4
⊢
(1...(𝑁 + 1)) ∈
V | 
| 37 |  | elmapg 8879 | . . . 4
⊢ ((𝐵 ∈ V ∧ (1...(𝑁 + 1)) ∈ V) → ((𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}) ∈ (𝐵 ↑m (1...(𝑁 + 1))) ↔ (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):(1...(𝑁 + 1))⟶𝐵)) | 
| 38 | 4, 36, 37 | sylancl 586 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → ((𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}) ∈ (𝐵 ↑m (1...(𝑁 + 1))) ↔ (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}):(1...(𝑁 + 1))⟶𝐵)) | 
| 39 | 35, 38 | mpbird 257 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}) ∈ (𝐵 ↑m (1...(𝑁 + 1)))) | 
| 40 |  | mapfzcons.1 | . . . . 5
⊢ 𝑀 = (𝑁 + 1) | 
| 41 | 40 | opeq1i 4876 | . . . 4
⊢
〈𝑀, 𝐶〉 = 〈(𝑁 + 1), 𝐶〉 | 
| 42 | 41 | sneqi 4637 | . . 3
⊢
{〈𝑀, 𝐶〉} = {〈(𝑁 + 1), 𝐶〉} | 
| 43 | 42 | uneq2i 4165 | . 2
⊢ (𝐴 ∪ {〈𝑀, 𝐶〉}) = (𝐴 ∪ {〈(𝑁 + 1), 𝐶〉}) | 
| 44 | 40 | oveq2i 7442 | . . 3
⊢
(1...𝑀) =
(1...(𝑁 +
1)) | 
| 45 | 44 | oveq2i 7442 | . 2
⊢ (𝐵 ↑m (1...𝑀)) = (𝐵 ↑m (1...(𝑁 + 1))) | 
| 46 | 39, 43, 45 | 3eltr4g 2858 | 1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ (𝐵 ↑m (1...𝑁)) ∧ 𝐶 ∈ 𝐵) → (𝐴 ∪ {〈𝑀, 𝐶〉}) ∈ (𝐵 ↑m (1...𝑀))) |