Step |
Hyp |
Ref |
Expression |
1 |
|
sge0f1o.1 |
⊢ Ⅎ 𝑘 𝜑 |
2 |
|
sge0f1o.2 |
⊢ Ⅎ 𝑛 𝜑 |
3 |
|
sge0f1o.3 |
⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 ) |
4 |
|
sge0f1o.4 |
⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) |
5 |
|
sge0f1o.5 |
⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 ) |
6 |
|
sge0f1o.6 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 ) |
7 |
|
sge0f1o.7 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) |
8 |
|
f1ofo |
⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 –onto→ 𝐴 ) |
9 |
5 8
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝐶 –onto→ 𝐴 ) |
10 |
|
focdmex |
⊢ ( 𝐶 ∈ 𝑉 → ( 𝐹 : 𝐶 –onto→ 𝐴 → 𝐴 ∈ V ) ) |
11 |
4 9 10
|
sylc |
⊢ ( 𝜑 → 𝐴 ∈ V ) |
12 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → 𝐴 ∈ V ) |
13 |
1 7
|
fmptd2f |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) ) |
15 |
|
nfv |
⊢ Ⅎ 𝑛 +∞ ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) |
16 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷 ) → +∞ = 𝐷 ) |
17 |
|
f1of |
⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 ⟶ 𝐴 ) |
18 |
5 17
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐴 ) |
19 |
18
|
ffvelcdmda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) |
20 |
|
nfv |
⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑛 ) = 𝐺 |
21 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 |
22 |
21
|
nfeq1 |
⊢ Ⅎ 𝑘 ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐷 |
23 |
20 22
|
nfim |
⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑛 ) = 𝐺 → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐷 ) |
24 |
|
eqeq1 |
⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → ( 𝑘 = 𝐺 ↔ ( 𝐹 ‘ 𝑛 ) = 𝐺 ) ) |
25 |
|
csbeq1a |
⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → 𝐵 = ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) |
26 |
25
|
eqeq1d |
⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → ( 𝐵 = 𝐷 ↔ ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐷 ) ) |
27 |
24 26
|
imbi12d |
⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → ( ( 𝑘 = 𝐺 → 𝐵 = 𝐷 ) ↔ ( ( 𝐹 ‘ 𝑛 ) = 𝐺 → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐷 ) ) ) |
28 |
23 27 3
|
vtoclg1f |
⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 → ( ( 𝐹 ‘ 𝑛 ) = 𝐺 → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐷 ) ) |
29 |
19 6 28
|
sylc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐷 ) |
30 |
29
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐷 = ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) |
31 |
30
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷 ) → 𝐷 = ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) |
32 |
16 31
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷 ) → +∞ = ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) |
33 |
|
simpl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝜑 ) |
34 |
33 19
|
jca |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝜑 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) ) |
35 |
|
nfv |
⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 |
36 |
1 35
|
nfan |
⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) |
37 |
21
|
nfel1 |
⊢ Ⅎ 𝑘 ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) |
38 |
36 37
|
nfim |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) |
39 |
|
eleq1 |
⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → ( 𝑘 ∈ 𝐴 ↔ ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) ) |
40 |
39
|
anbi2d |
⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) ) ) |
41 |
25
|
eleq1d |
⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → ( 𝐵 ∈ ( 0 [,] +∞ ) ↔ ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) ) |
42 |
40 41
|
imbi12d |
⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) ) ↔ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) ) ) |
43 |
38 42 7
|
vtoclg1f |
⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) ) |
44 |
19 34 43
|
sylc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) |
45 |
|
eqid |
⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) |
46 |
21 45 25
|
elrnmpt1sf |
⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 ∧ ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ( 0 [,] +∞ ) ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
47 |
19 44 46
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
48 |
47
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷 ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
49 |
32 48
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ +∞ = 𝐷 ) → +∞ ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
50 |
49
|
3exp |
⊢ ( 𝜑 → ( 𝑛 ∈ 𝐶 → ( +∞ = 𝐷 → +∞ ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) ) |
51 |
2 15 50
|
rexlimd |
⊢ ( 𝜑 → ( ∃ 𝑛 ∈ 𝐶 +∞ = 𝐷 → +∞ ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) |
52 |
|
pnfex |
⊢ +∞ ∈ V |
53 |
|
eqid |
⊢ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) |
54 |
53
|
elrnmpt |
⊢ ( +∞ ∈ V → ( +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ↔ ∃ 𝑛 ∈ 𝐶 +∞ = 𝐷 ) ) |
55 |
52 54
|
ax-mp |
⊢ ( +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ↔ ∃ 𝑛 ∈ 𝐶 +∞ = 𝐷 ) |
56 |
55
|
biimpi |
⊢ ( +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) → ∃ 𝑛 ∈ 𝐶 +∞ = 𝐷 ) |
57 |
51 56
|
impel |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → +∞ ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
58 |
12 14 57
|
sge0pnfval |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ ) |
59 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → 𝐶 ∈ 𝑉 ) |
60 |
30 44
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐷 ∈ ( 0 [,] +∞ ) ) |
61 |
2 60
|
fmptd2f |
⊢ ( 𝜑 → ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) : 𝐶 ⟶ ( 0 [,] +∞ ) ) |
62 |
61
|
adantr |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) : 𝐶 ⟶ ( 0 [,] +∞ ) ) |
63 |
|
simpr |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
64 |
59 62 63
|
sge0pnfval |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) = +∞ ) |
65 |
58 64
|
eqtr4d |
⊢ ( ( 𝜑 ∧ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ) |
66 |
|
sumex |
⊢ Σ 𝑘 ∈ 𝑦 𝐵 ∈ V |
67 |
66
|
a1i |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐵 ∈ V ) |
68 |
|
cnvimass |
⊢ ( ◡ 𝐹 “ 𝑦 ) ⊆ dom 𝐹 |
69 |
68 18
|
fssdm |
⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝐶 ) |
70 |
4 69
|
sselpwd |
⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝒫 𝐶 ) |
71 |
70
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝒫 𝐶 ) |
72 |
|
f1ocnv |
⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 ) |
73 |
5 72
|
syl |
⊢ ( 𝜑 → ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 ) |
74 |
|
f1ofun |
⊢ ( ◡ 𝐹 : 𝐴 –1-1-onto→ 𝐶 → Fun ◡ 𝐹 ) |
75 |
73 74
|
syl |
⊢ ( 𝜑 → Fun ◡ 𝐹 ) |
76 |
|
elinel2 |
⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin ) |
77 |
|
imafi |
⊢ ( ( Fun ◡ 𝐹 ∧ 𝑦 ∈ Fin ) → ( ◡ 𝐹 “ 𝑦 ) ∈ Fin ) |
78 |
75 76 77
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ Fin ) |
79 |
71 78
|
elind |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) |
80 |
79
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) |
81 |
|
nfv |
⊢ Ⅎ 𝑘 ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) |
82 |
1 81
|
nfan |
⊢ Ⅎ 𝑘 ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
83 |
|
nfv |
⊢ Ⅎ 𝑘 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) |
84 |
82 83
|
nfan |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
85 |
|
nfmpt1 |
⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) |
86 |
85
|
nfrn |
⊢ Ⅎ 𝑛 ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) |
87 |
86
|
nfel2 |
⊢ Ⅎ 𝑛 +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) |
88 |
87
|
nfn |
⊢ Ⅎ 𝑛 ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) |
89 |
2 88
|
nfan |
⊢ Ⅎ 𝑛 ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
90 |
|
nfv |
⊢ Ⅎ 𝑛 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) |
91 |
89 90
|
nfan |
⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
92 |
78
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ Fin ) |
93 |
|
f1of1 |
⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 –1-1→ 𝐴 ) |
94 |
5 93
|
syl |
⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1→ 𝐴 ) |
95 |
94
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 : 𝐶 –1-1→ 𝐴 ) |
96 |
69
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝐶 ) |
97 |
|
f1ores |
⊢ ( ( 𝐹 : 𝐶 –1-1→ 𝐴 ∧ ( ◡ 𝐹 “ 𝑦 ) ⊆ 𝐶 ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) : ( ◡ 𝐹 “ 𝑦 ) –1-1-onto→ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) |
98 |
95 96 97
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) : ( ◡ 𝐹 “ 𝑦 ) –1-1-onto→ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) |
99 |
|
elpwinss |
⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 ) |
100 |
|
foimacnv |
⊢ ( ( 𝐹 : 𝐶 –onto→ 𝐴 ∧ 𝑦 ⊆ 𝐴 ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 ) |
101 |
9 99 100
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) = 𝑦 ) |
102 |
101
|
f1oeq3d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) : ( ◡ 𝐹 “ 𝑦 ) –1-1-onto→ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ↔ ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) : ( ◡ 𝐹 “ 𝑦 ) –1-1-onto→ 𝑦 ) ) |
103 |
98 102
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) : ( ◡ 𝐹 “ 𝑦 ) –1-1-onto→ 𝑦 ) |
104 |
103
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) : ( ◡ 𝐹 “ 𝑦 ) –1-1-onto→ 𝑦 ) |
105 |
18 4
|
fexd |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
106 |
|
cnvexg |
⊢ ( 𝐹 ∈ V → ◡ 𝐹 ∈ V ) |
107 |
105 106
|
syl |
⊢ ( 𝜑 → ◡ 𝐹 ∈ V ) |
108 |
107
|
imaexd |
⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝑦 ) ∈ V ) |
109 |
108
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ V ) |
110 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → 𝜑 ) |
111 |
79
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) |
112 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) |
113 |
110 111 112
|
jca31 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( ( 𝜑 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) ) |
114 |
|
eleq1 |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ) |
115 |
114
|
anbi2d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ↔ ( 𝜑 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ) ) |
116 |
|
eleq2w2 |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝑛 ∈ 𝑥 ↔ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) ) |
117 |
115 116
|
anbi12d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑥 ) ↔ ( ( 𝜑 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) ) ) |
118 |
|
reseq2 |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) ) |
119 |
118
|
fveq1d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑛 ) = ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) ‘ 𝑛 ) ) |
120 |
119
|
eqeq1d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑛 ) = 𝐺 ↔ ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) ‘ 𝑛 ) = 𝐺 ) ) |
121 |
117 120
|
imbi12d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑛 ) = 𝐺 ) ↔ ( ( ( 𝜑 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) ‘ 𝑛 ) = 𝐺 ) ) ) |
122 |
|
fvres |
⊢ ( 𝑛 ∈ 𝑥 → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) |
123 |
122
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) ) |
124 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑥 ) → 𝜑 ) |
125 |
|
elpwinss |
⊢ ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑥 ⊆ 𝐶 ) |
126 |
125
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑥 ⊆ 𝐶 ) |
127 |
126
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑥 ) → 𝑛 ∈ 𝐶 ) |
128 |
124 127 6
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑥 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 ) |
129 |
123 128
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑛 ) = 𝐺 ) |
130 |
121 129
|
vtoclg |
⊢ ( ( ◡ 𝐹 “ 𝑦 ) ∈ V → ( ( ( 𝜑 ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) ‘ 𝑛 ) = 𝐺 ) ) |
131 |
109 113 130
|
sylc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) ‘ 𝑛 ) = 𝐺 ) |
132 |
131
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) ) → ( ( 𝐹 ↾ ( ◡ 𝐹 “ 𝑦 ) ) ‘ 𝑛 ) = 𝐺 ) |
133 |
108
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ V ) |
134 |
|
simpll |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ) |
135 |
70
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ 𝒫 𝐶 ) |
136 |
92
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ Fin ) |
137 |
135 136
|
elind |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) |
138 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ 𝑦 ) |
139 |
101
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) |
140 |
139
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑦 = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) |
141 |
138 140
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) |
142 |
141
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝑘 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) |
143 |
134 137 142
|
jca31 |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ) |
144 |
114
|
anbi2d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ↔ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ) ) |
145 |
|
imaeq2 |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) |
146 |
145
|
eleq2d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( 𝑘 ∈ ( 𝐹 “ 𝑥 ) ↔ 𝑘 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ) |
147 |
144 146
|
anbi12d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) ↔ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) ) ) |
148 |
147
|
imbi1d |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → ( ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → 𝐵 ∈ ℂ ) ↔ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) → 𝐵 ∈ ℂ ) ) ) |
149 |
|
rge0ssre |
⊢ ( 0 [,) +∞ ) ⊆ ℝ |
150 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
151 |
149 150
|
sstri |
⊢ ( 0 [,) +∞ ) ⊆ ℂ |
152 |
|
simplll |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → 𝜑 ) |
153 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
154 |
18
|
fimassd |
⊢ ( 𝜑 → ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) |
155 |
154
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → ( 𝐹 “ 𝑥 ) ⊆ 𝐴 ) |
156 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) |
157 |
155 156
|
sseldd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → 𝑘 ∈ 𝐴 ) |
158 |
157
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → 𝑘 ∈ 𝐴 ) |
159 |
|
foelcdmi |
⊢ ( ( 𝐹 : 𝐶 –onto→ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ∃ 𝑛 ∈ 𝐶 ( 𝐹 ‘ 𝑛 ) = 𝑘 ) |
160 |
9 159
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∃ 𝑛 ∈ 𝐶 ( 𝐹 ‘ 𝑛 ) = 𝑘 ) |
161 |
160
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑘 ∈ 𝐴 ) → ∃ 𝑛 ∈ 𝐶 ( 𝐹 ‘ 𝑛 ) = 𝑘 ) |
162 |
|
nfv |
⊢ Ⅎ 𝑛 𝑘 ∈ 𝐴 |
163 |
89 162
|
nfan |
⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑘 ∈ 𝐴 ) |
164 |
|
nfv |
⊢ Ⅎ 𝑛 𝐵 ∈ ( 0 [,) +∞ ) |
165 |
|
csbid |
⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐵 = 𝐵 |
166 |
165
|
eqcomi |
⊢ 𝐵 = ⦋ 𝑘 / 𝑘 ⦌ 𝐵 |
167 |
166
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑘 ) → 𝐵 = ⦋ 𝑘 / 𝑘 ⦌ 𝐵 ) |
168 |
|
id |
⊢ ( ( 𝐹 ‘ 𝑛 ) = 𝑘 → ( 𝐹 ‘ 𝑛 ) = 𝑘 ) |
169 |
168
|
eqcomd |
⊢ ( ( 𝐹 ‘ 𝑛 ) = 𝑘 → 𝑘 = ( 𝐹 ‘ 𝑛 ) ) |
170 |
169
|
csbeq1d |
⊢ ( ( 𝐹 ‘ 𝑛 ) = 𝑘 → ⦋ 𝑘 / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) |
171 |
170
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑘 ) → ⦋ 𝑘 / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) |
172 |
29
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑘 ) → ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐷 ) |
173 |
167 171 172
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑘 ) → 𝐵 = 𝐷 ) |
174 |
173
|
3adant1r |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑘 ) → 𝐵 = 𝐷 ) |
175 |
|
0xr |
⊢ 0 ∈ ℝ* |
176 |
175
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → 0 ∈ ℝ* ) |
177 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
178 |
177
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → +∞ ∈ ℝ* ) |
179 |
60
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → 𝐷 ∈ ( 0 [,] +∞ ) ) |
180 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) |
181 |
176 178 179 180
|
eliccnelico |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → 𝐷 = +∞ ) |
182 |
181
|
eqcomd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → +∞ = 𝐷 ) |
183 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝑛 ∈ 𝐶 ) |
184 |
53 183 60
|
elrnmpt1d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐷 ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
185 |
184
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → 𝐷 ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
186 |
182 185
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
187 |
186
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
188 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑛 ∈ 𝐶 ) ∧ ¬ 𝐷 ∈ ( 0 [,) +∞ ) ) → ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) |
189 |
187 188
|
condan |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑛 ∈ 𝐶 ) → 𝐷 ∈ ( 0 [,) +∞ ) ) |
190 |
189
|
3adant3 |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑘 ) → 𝐷 ∈ ( 0 [,) +∞ ) ) |
191 |
174 190
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑛 ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑛 ) = 𝑘 ) → 𝐵 ∈ ( 0 [,) +∞ ) ) |
192 |
191
|
3exp |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( 𝑛 ∈ 𝐶 → ( ( 𝐹 ‘ 𝑛 ) = 𝑘 → 𝐵 ∈ ( 0 [,) +∞ ) ) ) ) |
193 |
192
|
adantr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑛 ∈ 𝐶 → ( ( 𝐹 ‘ 𝑛 ) = 𝑘 → 𝐵 ∈ ( 0 [,) +∞ ) ) ) ) |
194 |
163 164 193
|
rexlimd |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ∃ 𝑛 ∈ 𝐶 ( 𝐹 ‘ 𝑛 ) = 𝑘 → 𝐵 ∈ ( 0 [,) +∞ ) ) ) |
195 |
161 194
|
mpd |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) ) |
196 |
152 153 158 195
|
syl21anc |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → 𝐵 ∈ ( 0 [,) +∞ ) ) |
197 |
151 196
|
sselid |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ 𝑥 ) ) → 𝐵 ∈ ℂ ) |
198 |
148 197
|
vtoclg |
⊢ ( ( ◡ 𝐹 “ 𝑦 ) ∈ V → ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑦 ) ) ) → 𝐵 ∈ ℂ ) ) |
199 |
133 143 198
|
sylc |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑘 ∈ 𝑦 ) → 𝐵 ∈ ℂ ) |
200 |
84 91 3 92 104 132 199
|
fsumf1of |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ 𝑘 ∈ 𝑦 𝐵 = Σ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) 𝐷 ) |
201 |
|
sumeq1 |
⊢ ( 𝑥 = ( ◡ 𝐹 “ 𝑦 ) → Σ 𝑛 ∈ 𝑥 𝐷 = Σ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) 𝐷 ) |
202 |
201
|
rspceeqv |
⊢ ( ( ( ◡ 𝐹 “ 𝑦 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ Σ 𝑘 ∈ 𝑦 𝐵 = Σ 𝑛 ∈ ( ◡ 𝐹 “ 𝑦 ) 𝐷 ) → ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) Σ 𝑘 ∈ 𝑦 𝐵 = Σ 𝑛 ∈ 𝑥 𝐷 ) |
203 |
80 200 202
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∃ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) Σ 𝑘 ∈ 𝑦 𝐵 = Σ 𝑛 ∈ 𝑥 𝐷 ) |
204 |
67 203
|
rnmptssrn |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 𝐷 ) ) |
205 |
|
sumex |
⊢ Σ 𝑛 ∈ 𝑥 𝐷 ∈ V |
206 |
205
|
a1i |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → Σ 𝑛 ∈ 𝑥 𝐷 ∈ V ) |
207 |
11 154
|
sselpwd |
⊢ ( 𝜑 → ( 𝐹 “ 𝑥 ) ∈ 𝒫 𝐴 ) |
208 |
207
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 “ 𝑥 ) ∈ 𝒫 𝐴 ) |
209 |
18
|
ffund |
⊢ ( 𝜑 → Fun 𝐹 ) |
210 |
|
elinel2 |
⊢ ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑥 ∈ Fin ) |
211 |
|
imafi |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ Fin ) → ( 𝐹 “ 𝑥 ) ∈ Fin ) |
212 |
209 210 211
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 “ 𝑥 ) ∈ Fin ) |
213 |
208 212
|
elind |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 “ 𝑥 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
214 |
213
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 “ 𝑥 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
215 |
|
nfv |
⊢ Ⅎ 𝑘 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) |
216 |
82 215
|
nfan |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) |
217 |
|
nfv |
⊢ Ⅎ 𝑛 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) |
218 |
89 217
|
nfan |
⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) |
219 |
210
|
adantl |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑥 ∈ Fin ) |
220 |
|
f1ores |
⊢ ( ( 𝐹 : 𝐶 –1-1→ 𝐴 ∧ 𝑥 ⊆ 𝐶 ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ( 𝐹 “ 𝑥 ) ) |
221 |
94 125 220
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ( 𝐹 “ 𝑥 ) ) |
222 |
221
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ( 𝐹 “ 𝑥 ) ) |
223 |
129
|
adantllr |
⊢ ( ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑥 ) ‘ 𝑛 ) = 𝐺 ) |
224 |
216 218 3 219 222 223 197
|
fsumf1of |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → Σ 𝑘 ∈ ( 𝐹 “ 𝑥 ) 𝐵 = Σ 𝑛 ∈ 𝑥 𝐷 ) |
225 |
224
|
eqcomd |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → Σ 𝑛 ∈ 𝑥 𝐷 = Σ 𝑘 ∈ ( 𝐹 “ 𝑥 ) 𝐵 ) |
226 |
|
sumeq1 |
⊢ ( 𝑦 = ( 𝐹 “ 𝑥 ) → Σ 𝑘 ∈ 𝑦 𝐵 = Σ 𝑘 ∈ ( 𝐹 “ 𝑥 ) 𝐵 ) |
227 |
226
|
rspceeqv |
⊢ ( ( ( 𝐹 “ 𝑥 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ Σ 𝑛 ∈ 𝑥 𝐷 = Σ 𝑘 ∈ ( 𝐹 “ 𝑥 ) 𝐵 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑛 ∈ 𝑥 𝐷 = Σ 𝑘 ∈ 𝑦 𝐵 ) |
228 |
214 225 227
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) Σ 𝑛 ∈ 𝑥 𝐷 = Σ 𝑘 ∈ 𝑦 𝐵 ) |
229 |
206 228
|
rnmptssrn |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 𝐷 ) ⊆ ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) ) |
230 |
204 229
|
eqssd |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) = ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 𝐷 ) ) |
231 |
230
|
supeq1d |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 𝐷 ) , ℝ* , < ) ) |
232 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → 𝐴 ∈ V ) |
233 |
82 232 195
|
sge0revalmpt |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ Σ 𝑘 ∈ 𝑦 𝐵 ) , ℝ* , < ) ) |
234 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → 𝐶 ∈ 𝑉 ) |
235 |
89 234 189
|
sge0revalmpt |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ Σ 𝑛 ∈ 𝑥 𝐷 ) , ℝ* , < ) ) |
236 |
231 233 235
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ ran ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ) |
237 |
65 236
|
pm2.61dan |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) ) |