Proof of Theorem fsuppmapnn0fiub0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fsuppmapnn0fiubex 14034 | . 2
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚))) | 
| 2 |  | ssel2 3977 | . . . . . . . . . . . . . 14
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑓 ∈ 𝑀) → 𝑓 ∈ (𝑅 ↑m
ℕ0)) | 
| 3 | 2 | ancoms 458 | . . . . . . . . . . . . 13
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑀 ⊆ (𝑅 ↑m ℕ0))
→ 𝑓 ∈ (𝑅 ↑m
ℕ0)) | 
| 4 |  | elmapfn 8906 | . . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑅 ↑m ℕ0)
→ 𝑓 Fn
ℕ0) | 
| 5 | 3, 4 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑀 ⊆ (𝑅 ↑m ℕ0))
→ 𝑓 Fn
ℕ0) | 
| 6 | 5 | expcom 413 | . . . . . . . . . . 11
⊢ (𝑀 ⊆ (𝑅 ↑m ℕ0)
→ (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) | 
| 7 | 6 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) | 
| 8 | 7 | adantr 480 | . . . . . . . . 9
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) → (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) | 
| 9 | 8 | imp 406 | . . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → 𝑓 Fn ℕ0) | 
| 10 |  | nn0ex 12534 | . . . . . . . . 9
⊢
ℕ0 ∈ V | 
| 11 | 10 | a1i 11 | . . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ℕ0 ∈
V) | 
| 12 |  | simpll3 1214 | . . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → 𝑍 ∈ 𝑉) | 
| 13 |  | suppvalfn 8194 | . . . . . . . 8
⊢ ((𝑓 Fn ℕ0 ∧
ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉) → (𝑓 supp 𝑍) = {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍}) | 
| 14 | 9, 11, 12, 13 | syl3anc 1372 | . . . . . . 7
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) = {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍}) | 
| 15 | 14 | sseq1d 4014 | . . . . . 6
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍} ⊆ (0...𝑚))) | 
| 16 |  | rabss 4071 | . . . . . 6
⊢ ({𝑥 ∈ ℕ0
∣ (𝑓‘𝑥) ≠ 𝑍} ⊆ (0...𝑚) ↔ ∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚))) | 
| 17 | 15, 16 | bitrdi 287 | . . . . 5
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ ∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)))) | 
| 18 |  | nne 2943 | . . . . . . . . . 10
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 ↔ (𝑓‘𝑥) = 𝑍) | 
| 19 | 18 | biimpi 216 | . . . . . . . . 9
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 → (𝑓‘𝑥) = 𝑍) | 
| 20 | 19 | 2a1d 26 | . . . . . . . 8
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 → (((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 21 |  | elfz2nn0 13659 | . . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑚) ↔ (𝑥 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0
∧ 𝑥 ≤ 𝑚)) | 
| 22 |  | nn0re 12537 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) | 
| 23 |  | nn0re 12537 | . . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) | 
| 24 |  | lenlt 11340 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ) → (𝑥 ≤ 𝑚 ↔ ¬ 𝑚 < 𝑥)) | 
| 25 | 22, 23, 24 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑥 ≤ 𝑚 ↔ ¬ 𝑚 < 𝑥)) | 
| 26 |  | pm2.21 123 | . . . . . . . . . . . 12
⊢ (¬
𝑚 < 𝑥 → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍)) | 
| 27 | 25, 26 | biimtrdi 253 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑥 ≤ 𝑚 → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 28 | 27 | 3impia 1117 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0 ∧ 𝑥
≤ 𝑚) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍)) | 
| 29 | 28 | a1d 25 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0 ∧ 𝑥
≤ 𝑚) → (((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 30 | 21, 29 | sylbi 217 | . . . . . . . 8
⊢ (𝑥 ∈ (0...𝑚) → (((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 31 | 20, 30 | ja 186 | . . . . . . 7
⊢ (((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)) → (((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 32 | 31 | com12 32 | . . . . . 6
⊢
(((((𝑀 ⊆
(𝑅 ↑m
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 33 | 32 | ralimdva 3166 | . . . . 5
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → (∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)) → ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 34 | 17, 33 | sylbid 240 | . . . 4
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) → ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 35 | 34 | ralimdva 3166 | . . 3
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) →
(∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) → ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 36 | 35 | reximdva 3167 | . 2
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) | 
| 37 | 1, 36 | syld 47 | 1
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |