Proof of Theorem fsuppmapnn0fiub0
Step | Hyp | Ref
| Expression |
1 | | fsuppmapnn0fiubex 12792 |
. 2
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚))) |
2 | | ssel2 3598 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑓 ∈ 𝑀) → 𝑓 ∈ (𝑅 ↑𝑚
ℕ0)) |
3 | 2 | ancoms 469 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑀 ⊆ (𝑅 ↑𝑚
ℕ0)) → 𝑓 ∈ (𝑅 ↑𝑚
ℕ0)) |
4 | | elmapfn 7880 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (𝑅 ↑𝑚
ℕ0) → 𝑓 Fn ℕ0) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑀 ∧ 𝑀 ⊆ (𝑅 ↑𝑚
ℕ0)) → 𝑓 Fn ℕ0) |
6 | 5 | expcom 451 |
. . . . . . . . . . 11
⊢ (𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) → (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) |
7 | 6 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) |
8 | 7 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) → (𝑓 ∈ 𝑀 → 𝑓 Fn ℕ0)) |
9 | 8 | imp 445 |
. . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → 𝑓 Fn ℕ0) |
10 | | nn0ex 11298 |
. . . . . . . . 9
⊢
ℕ0 ∈ V |
11 | 10 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ℕ0 ∈
V) |
12 | | simpll3 1102 |
. . . . . . . 8
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → 𝑍 ∈ 𝑉) |
13 | | suppvalfn 7302 |
. . . . . . . 8
⊢ ((𝑓 Fn ℕ0 ∧
ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉) → (𝑓 supp 𝑍) = {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍}) |
14 | 9, 11, 12, 13 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → (𝑓 supp 𝑍) = {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍}) |
15 | 14 | sseq1d 3632 |
. . . . . 6
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ {𝑥 ∈ ℕ0 ∣ (𝑓‘𝑥) ≠ 𝑍} ⊆ (0...𝑚))) |
16 | | rabss 3679 |
. . . . . 6
⊢ ({𝑥 ∈ ℕ0
∣ (𝑓‘𝑥) ≠ 𝑍} ⊆ (0...𝑚) ↔ ∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚))) |
17 | 15, 16 | syl6bb 276 |
. . . . 5
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) ↔ ∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)))) |
18 | | nne 2798 |
. . . . . . . . . 10
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 ↔ (𝑓‘𝑥) = 𝑍) |
19 | 18 | biimpi 206 |
. . . . . . . . 9
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 → (𝑓‘𝑥) = 𝑍) |
20 | 19 | 2a1d 26 |
. . . . . . . 8
⊢ (¬
(𝑓‘𝑥) ≠ 𝑍 → (((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
21 | | elfz2nn0 12431 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑚) ↔ (𝑥 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0
∧ 𝑥 ≤ 𝑚)) |
22 | | nn0re 11301 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) |
23 | | nn0re 11301 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
24 | | lenlt 10116 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 𝑚 ∈ ℝ) → (𝑥 ≤ 𝑚 ↔ ¬ 𝑚 < 𝑥)) |
25 | 22, 23, 24 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑥 ≤ 𝑚 ↔ ¬ 𝑚 < 𝑥)) |
26 | | pm2.21 120 |
. . . . . . . . . . . 12
⊢ (¬
𝑚 < 𝑥 → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍)) |
27 | 25, 26 | syl6bi 243 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑥 ≤ 𝑚 → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
28 | 27 | 3impia 1261 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0 ∧ 𝑥
≤ 𝑚) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍)) |
29 | 28 | a1d 25 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℕ0
∧ 𝑚 ∈
ℕ0 ∧ 𝑥
≤ 𝑚) → (((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
30 | 21, 29 | sylbi 207 |
. . . . . . . 8
⊢ (𝑥 ∈ (0...𝑚) → (((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
31 | 20, 30 | ja 173 |
. . . . . . 7
⊢ (((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)) → (((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
32 | 31 | com12 32 |
. . . . . 6
⊢
(((((𝑀 ⊆
(𝑅
↑𝑚 ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) ∧ 𝑥 ∈ ℕ0) → (((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)) → (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
33 | 32 | ralimdva 2962 |
. . . . 5
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → (∀𝑥 ∈ ℕ0 ((𝑓‘𝑥) ≠ 𝑍 → 𝑥 ∈ (0...𝑚)) → ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
34 | 17, 33 | sylbid 230 |
. . . 4
⊢ ((((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) ∧ 𝑓 ∈ 𝑀) → ((𝑓 supp 𝑍) ⊆ (0...𝑚) → ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
35 | 34 | ralimdva 2962 |
. . 3
⊢ (((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) ∧ 𝑚 ∈ ℕ0) →
(∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) → ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
36 | 35 | reximdva 3017 |
. 2
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 (𝑓 supp 𝑍) ⊆ (0...𝑚) → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |
37 | 1, 36 | syld 47 |
1
⊢ ((𝑀 ⊆ (𝑅 ↑𝑚
ℕ0) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉) → (∀𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∃𝑚 ∈ ℕ0 ∀𝑓 ∈ 𝑀 ∀𝑥 ∈ ℕ0 (𝑚 < 𝑥 → (𝑓‘𝑥) = 𝑍))) |