Proof of Theorem fsuppmapnn0fiub0
Step | Hyp | Ref
| Expression |
1 | | fsuppmapnn0fiubex 13712 |
. 2
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚))) |
2 | | ssel2 3916 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑓 ∈ 𝑀) → 𝑓 ∈ (𝑅 ↑m
ℕ0)) |
3 | 2 | ancoms 459 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑀 ⊆ (𝑅 ↑m ℕ0))
→ 𝑓 ∈ (𝑅 ↑m
ℕ0)) |
4 | | elmapfn 8653 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑅 ↑m ℕ0)
→ 𝑓 Fn
ℕ0) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑀 ⊆ (𝑅 ↑m ℕ0))
→ 𝑓 Fn
ℕ0) |
6 | 5 | expcom 414 |
. . . . . . . . . . 11
⊢ (𝑀 ⊆ (𝑅 ↑m ℕ0)
→ (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) |
7 | 6 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) |
8 | 7 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) → (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) |
9 | 8 | imp 407 |
. . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → 𝑓 Fn ℕ0) |
10 | | nn0ex 12239 |
. . . . . . . . 9
⊢
ℕ0 ∈ V |
11 | 10 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ℕ0 ∈
V) |
12 | | simpll3 1213 |
. . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → 𝑍 ∈ 𝑉) |
13 | | suppvalfn 7985 |
. . . . . . . 8
⊢ ((𝑓 Fn ℕ0 ∧
ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉) → (𝑓 supp 𝑍) = {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍}) |
14 | 9, 11, 12, 13 | syl3anc 1370 |
. . . . . . 7
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) = {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍}) |
15 | 14 | sseq1d 3952 |
. . . . . 6
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍} ⊆ (0...𝑚))) |
16 | | rabss 4005 |
. . . . . 6
⊢ ({𝑥 ∈ ℕ0
∣ (𝑓‘𝑥) ≠ 𝑍} ⊆ (0...𝑚) ↔ ∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚))) |
17 | 15, 16 | bitrdi 287 |
. . . . 5
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ ∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)))) |
18 | | nne 2947 |
. . . . . . . . . 10
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 ↔ (𝑓‘𝑥) = 𝑍) |
19 | 18 | biimpi 215 |
. . . . . . . . 9
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 → (𝑓‘𝑥) = 𝑍) |
20 | 19 | 2a1d 26 |
. . . . . . . 8
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 → (((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
21 | | elfz2nn0 13347 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑚) ↔ (𝑥 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0
∧ 𝑥 ≤ 𝑚)) |
22 | | nn0re 12242 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) |
23 | | nn0re 12242 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
24 | | lenlt 11053 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ) → (𝑥 ≤ 𝑚 ↔ ¬ 𝑚 < 𝑥)) |
25 | 22, 23, 24 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑥 ≤ 𝑚 ↔ ¬ 𝑚 < 𝑥)) |
26 | | pm2.21 123 |
. . . . . . . . . . . 12
⊢ (¬
𝑚 < 𝑥 → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍)) |
27 | 25, 26 | syl6bi 252 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑥 ≤ 𝑚 → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
28 | 27 | 3impia 1116 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0 ∧ 𝑥
≤ 𝑚) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍)) |
29 | 28 | a1d 25 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0 ∧ 𝑥
≤ 𝑚) → (((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
30 | 21, 29 | sylbi 216 |
. . . . . . . 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 3108 |
. . . . 5
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → (∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)) → ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
34 | 17, 33 | sylbid 239 |
. . . 4
⊢ ((((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) → ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
35 | 34 | ralimdva 3108 |
. . 3
⊢ (((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) →
(∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) → ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
36 | 35 | reximdva 3203 |
. 2
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
37 | 1, 36 | syld 47 |
1
⊢ ((𝑀 ⊆ (𝑅 ↑m ℕ0)
∧ 𝑀 ∈ Fin ∧
𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |