Step |
Hyp |
Ref |
Expression |
1 |
|
fsuppmapnn0fiub.u |
⊢ 𝑈 = ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) |
2 |
|
fsuppmapnn0fiub.s |
⊢ 𝑆 = sup ( 𝑈 , ℝ , < ) |
3 |
|
nfv |
⊢ Ⅎ 𝑓 ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) |
4 |
|
nfra1 |
⊢ Ⅎ 𝑓 ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 |
5 |
|
nfv |
⊢ Ⅎ 𝑓 𝑈 ≠ ∅ |
6 |
4 5
|
nfan |
⊢ Ⅎ 𝑓 ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) |
7 |
3 6
|
nfan |
⊢ Ⅎ 𝑓 ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) |
8 |
|
suppssdm |
⊢ ( 𝑓 supp 𝑍 ) ⊆ dom 𝑓 |
9 |
|
ssel2 |
⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → 𝑓 ∈ ( 𝑅 ↑m ℕ0 ) ) |
10 |
|
elmapfn |
⊢ ( 𝑓 ∈ ( 𝑅 ↑m ℕ0 ) → 𝑓 Fn ℕ0 ) |
11 |
|
fndm |
⊢ ( 𝑓 Fn ℕ0 → dom 𝑓 = ℕ0 ) |
12 |
|
eqimss |
⊢ ( dom 𝑓 = ℕ0 → dom 𝑓 ⊆ ℕ0 ) |
13 |
11 12
|
syl |
⊢ ( 𝑓 Fn ℕ0 → dom 𝑓 ⊆ ℕ0 ) |
14 |
9 10 13
|
3syl |
⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 ⊆ ℕ0 ) |
15 |
14
|
3ad2antl1 |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 ⊆ ℕ0 ) |
16 |
8 15
|
sstrid |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ℕ0 ) |
17 |
16
|
sseld |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ℕ0 ) ) |
18 |
17
|
adantlr |
⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ℕ0 ) ) |
19 |
18
|
imp |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ ℕ0 ) |
20 |
1 2
|
fsuppmapnn0fiublem |
⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → 𝑆 ∈ ℕ0 ) ) |
21 |
20
|
imp |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → 𝑆 ∈ ℕ0 ) |
22 |
21
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑆 ∈ ℕ0 ) |
23 |
9 10 11
|
3syl |
⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 = ℕ0 ) |
24 |
23
|
ex |
⊢ ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) ) |
25 |
24
|
3ad2ant1 |
⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) ) |
26 |
25
|
adantr |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → dom 𝑓 = ℕ0 ) ) |
27 |
26
|
imp |
⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 = ℕ0 ) |
28 |
|
nn0ssre |
⊢ ℕ0 ⊆ ℝ |
29 |
27 28
|
eqsstrdi |
⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → dom 𝑓 ⊆ ℝ ) |
30 |
8 29
|
sstrid |
⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ℝ ) |
31 |
30
|
ex |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → ( 𝑓 supp 𝑍 ) ⊆ ℝ ) ) |
32 |
7 31
|
ralrimi |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ ) |
33 |
32
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ ) |
34 |
|
iunss |
⊢ ( ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ ↔ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ ) |
35 |
33 34
|
sylibr |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ℝ ) |
36 |
1 35
|
eqsstrid |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑈 ⊆ ℝ ) |
37 |
|
simp2 |
⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → 𝑀 ∈ Fin ) |
38 |
|
id |
⊢ ( 𝑓 finSupp 𝑍 → 𝑓 finSupp 𝑍 ) |
39 |
38
|
fsuppimpd |
⊢ ( 𝑓 finSupp 𝑍 → ( 𝑓 supp 𝑍 ) ∈ Fin ) |
40 |
39
|
ralimi |
⊢ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) |
41 |
40
|
adantr |
⊢ ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) |
42 |
37 41
|
anim12i |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑀 ∈ Fin ∧ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) ) |
43 |
42
|
ad2antrr |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ( 𝑀 ∈ Fin ∧ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) ) |
44 |
|
iunfi |
⊢ ( ( 𝑀 ∈ Fin ∧ ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) |
45 |
43 44
|
syl |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ∈ Fin ) |
46 |
1 45
|
eqeltrid |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑈 ∈ Fin ) |
47 |
|
rspe |
⊢ ( ( 𝑓 ∈ 𝑀 ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → ∃ 𝑓 ∈ 𝑀 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) |
48 |
|
eliun |
⊢ ( 𝑥 ∈ ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ↔ ∃ 𝑓 ∈ 𝑀 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) |
49 |
47 48
|
sylibr |
⊢ ( ( 𝑓 ∈ 𝑀 ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ ∪ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ) |
50 |
49 1
|
eleqtrrdi |
⊢ ( ( 𝑓 ∈ 𝑀 ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ 𝑈 ) |
51 |
50
|
adantll |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ 𝑈 ) |
52 |
2
|
a1i |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑆 = sup ( 𝑈 , ℝ , < ) ) |
53 |
36 46 51 52
|
supfirege |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ≤ 𝑆 ) |
54 |
|
elfz2nn0 |
⊢ ( 𝑥 ∈ ( 0 ... 𝑆 ) ↔ ( 𝑥 ∈ ℕ0 ∧ 𝑆 ∈ ℕ0 ∧ 𝑥 ≤ 𝑆 ) ) |
55 |
19 22 53 54
|
syl3anbrc |
⊢ ( ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) ∧ 𝑥 ∈ ( 𝑓 supp 𝑍 ) ) → 𝑥 ∈ ( 0 ... 𝑆 ) ) |
56 |
55
|
ex |
⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑥 ∈ ( 𝑓 supp 𝑍 ) → 𝑥 ∈ ( 0 ... 𝑆 ) ) ) |
57 |
56
|
ssrdv |
⊢ ( ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) ∧ 𝑓 ∈ 𝑀 ) → ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) |
58 |
57
|
ex |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ( 𝑓 ∈ 𝑀 → ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) ) |
59 |
7 58
|
ralrimi |
⊢ ( ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) ∧ ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) |
60 |
59
|
ex |
⊢ ( ( 𝑀 ⊆ ( 𝑅 ↑m ℕ0 ) ∧ 𝑀 ∈ Fin ∧ 𝑍 ∈ 𝑉 ) → ( ( ∀ 𝑓 ∈ 𝑀 𝑓 finSupp 𝑍 ∧ 𝑈 ≠ ∅ ) → ∀ 𝑓 ∈ 𝑀 ( 𝑓 supp 𝑍 ) ⊆ ( 0 ... 𝑆 ) ) ) |