Step |
Hyp |
Ref |
Expression |
1 |
|
offinsupp1.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
2 |
|
offinsupp1.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑈 ) |
3 |
|
offinsupp1.z |
⊢ ( 𝜑 → 𝑍 ∈ 𝑊 ) |
4 |
|
offinsupp1.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 ) |
5 |
|
offinsupp1.g |
⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑇 ) |
6 |
|
offinsupp1.1 |
⊢ ( 𝜑 → 𝐹 finSupp 𝑌 ) |
7 |
|
offinsupp1.2 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑌 𝑅 𝑥 ) = 𝑍 ) |
8 |
6
|
fsuppimpd |
⊢ ( 𝜑 → ( 𝐹 supp 𝑌 ) ∈ Fin ) |
9 |
|
ssidd |
⊢ ( 𝜑 → ( 𝐹 supp 𝑌 ) ⊆ ( 𝐹 supp 𝑌 ) ) |
10 |
9 7 4 5 1 2
|
suppssof1 |
⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑌 ) ) |
11 |
8 10
|
ssfid |
⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin ) |
12 |
|
ovexd |
⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑆 ∧ 𝑗 ∈ 𝑇 ) ) → ( 𝑖 𝑅 𝑗 ) ∈ V ) |
13 |
|
inidm |
⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |
14 |
12 4 5 1 1 13
|
off |
⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) : 𝐴 ⟶ V ) |
15 |
14
|
ffund |
⊢ ( 𝜑 → Fun ( 𝐹 ∘f 𝑅 𝐺 ) ) |
16 |
|
ovexd |
⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ V ) |
17 |
|
funisfsupp |
⊢ ( ( Fun ( 𝐹 ∘f 𝑅 𝐺 ) ∧ ( 𝐹 ∘f 𝑅 𝐺 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∘f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin ) ) |
18 |
15 16 3 17
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∘f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin ) ) |
19 |
11 18
|
mpbird |
⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) finSupp 𝑍 ) |