Step | Hyp | Ref
| Expression |
1 | | caonncan.a |
. . . . 5
⊢ (𝜑 → 𝐴:𝐼⟶𝑆) |
2 | 1 | ffvelrnda 6961 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐴‘𝑧) ∈ 𝑆) |
3 | | caonncan.b |
. . . . 5
⊢ (𝜑 → 𝐵:𝐼⟶𝑆) |
4 | 3 | ffvelrnda 6961 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐵‘𝑧) ∈ 𝑆) |
5 | | caonncan.z |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑀(𝑥𝑀𝑦)) = 𝑦) |
6 | 5 | ralrimivva 3123 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝑀(𝑥𝑀𝑦)) = 𝑦) |
7 | 6 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝑀(𝑥𝑀𝑦)) = 𝑦) |
8 | | id 22 |
. . . . . . 7
⊢ (𝑥 = (𝐴‘𝑧) → 𝑥 = (𝐴‘𝑧)) |
9 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = (𝐴‘𝑧) → (𝑥𝑀𝑦) = ((𝐴‘𝑧)𝑀𝑦)) |
10 | 8, 9 | oveq12d 7293 |
. . . . . 6
⊢ (𝑥 = (𝐴‘𝑧) → (𝑥𝑀(𝑥𝑀𝑦)) = ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀𝑦))) |
11 | 10 | eqeq1d 2740 |
. . . . 5
⊢ (𝑥 = (𝐴‘𝑧) → ((𝑥𝑀(𝑥𝑀𝑦)) = 𝑦 ↔ ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀𝑦)) = 𝑦)) |
12 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑦 = (𝐵‘𝑧) → ((𝐴‘𝑧)𝑀𝑦) = ((𝐴‘𝑧)𝑀(𝐵‘𝑧))) |
13 | 12 | oveq2d 7291 |
. . . . . 6
⊢ (𝑦 = (𝐵‘𝑧) → ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀𝑦)) = ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀(𝐵‘𝑧)))) |
14 | | id 22 |
. . . . . 6
⊢ (𝑦 = (𝐵‘𝑧) → 𝑦 = (𝐵‘𝑧)) |
15 | 13, 14 | eqeq12d 2754 |
. . . . 5
⊢ (𝑦 = (𝐵‘𝑧) → (((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀𝑦)) = 𝑦 ↔ ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀(𝐵‘𝑧))) = (𝐵‘𝑧))) |
16 | 11, 15 | rspc2va 3571 |
. . . 4
⊢ ((((𝐴‘𝑧) ∈ 𝑆 ∧ (𝐵‘𝑧) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝑀(𝑥𝑀𝑦)) = 𝑦) → ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀(𝐵‘𝑧))) = (𝐵‘𝑧)) |
17 | 2, 4, 7, 16 | syl21anc 835 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀(𝐵‘𝑧))) = (𝐵‘𝑧)) |
18 | 17 | mpteq2dva 5174 |
. 2
⊢ (𝜑 → (𝑧 ∈ 𝐼 ↦ ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀(𝐵‘𝑧)))) = (𝑧 ∈ 𝐼 ↦ (𝐵‘𝑧))) |
19 | | caonncan.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
20 | | fvexd 6789 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐴‘𝑧) ∈ V) |
21 | | ovexd 7310 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → ((𝐴‘𝑧)𝑀(𝐵‘𝑧)) ∈ V) |
22 | 1 | feqmptd 6837 |
. . 3
⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝐼 ↦ (𝐴‘𝑧))) |
23 | | fvexd 6789 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐵‘𝑧) ∈ V) |
24 | 3 | feqmptd 6837 |
. . . 4
⊢ (𝜑 → 𝐵 = (𝑧 ∈ 𝐼 ↦ (𝐵‘𝑧))) |
25 | 19, 20, 23, 22, 24 | offval2 7553 |
. . 3
⊢ (𝜑 → (𝐴 ∘f 𝑀𝐵) = (𝑧 ∈ 𝐼 ↦ ((𝐴‘𝑧)𝑀(𝐵‘𝑧)))) |
26 | 19, 20, 21, 22, 25 | offval2 7553 |
. 2
⊢ (𝜑 → (𝐴 ∘f 𝑀(𝐴 ∘f 𝑀𝐵)) = (𝑧 ∈ 𝐼 ↦ ((𝐴‘𝑧)𝑀((𝐴‘𝑧)𝑀(𝐵‘𝑧))))) |
27 | 18, 26, 24 | 3eqtr4d 2788 |
1
⊢ (𝜑 → (𝐴 ∘f 𝑀(𝐴 ∘f 𝑀𝐵)) = 𝐵) |