Step | Hyp | Ref
| Expression |
1 | | coapm.o |
. . . . . 6
⊢ · =
(compa‘𝐶) |
2 | | coapm.a |
. . . . . 6
⊢ 𝐴 = (Arrow‘𝐶) |
3 | | eqid 2738 |
. . . . . 6
⊢
(comp‘𝐶) =
(comp‘𝐶) |
4 | 1, 2, 3 | coafval 17429 |
. . . . 5
⊢ · =
(𝑔 ∈ 𝐴, 𝑓 ∈ {ℎ ∈ 𝐴 ∣ (coda‘ℎ) =
(doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉(comp‘𝐶)(coda‘𝑔))(2nd ‘𝑓))〉) |
5 | 4 | mpofun 7284 |
. . . 4
⊢ Fun · |
6 | | funfn 6363 |
. . . 4
⊢ (Fun
·
↔ · Fn dom ·
) |
7 | 5, 6 | mpbi 233 |
. . 3
⊢ · Fn dom
· |
8 | 1, 2 | dmcoass 17431 |
. . . . . . . . 9
⊢ dom ·
⊆ (𝐴 × 𝐴) |
9 | 8 | sseli 3871 |
. . . . . . . 8
⊢ (𝑧 ∈ dom · → 𝑧 ∈ (𝐴 × 𝐴)) |
10 | | 1st2nd2 7746 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 × 𝐴) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ dom · → 𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
12 | 11 | fveq2d 6672 |
. . . . . 6
⊢ (𝑧 ∈ dom · → ( ·
‘𝑧) = ( ·
‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
13 | | df-ov 7167 |
. . . . . 6
⊢
((1st ‘𝑧) · (2nd
‘𝑧)) = ( ·
‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
14 | 12, 13 | eqtr4di 2791 |
. . . . 5
⊢ (𝑧 ∈ dom · → ( ·
‘𝑧) =
((1st ‘𝑧)
·
(2nd ‘𝑧))) |
15 | | eqid 2738 |
. . . . . . 7
⊢
(Homa‘𝐶) = (Homa‘𝐶) |
16 | 2, 15 | homarw 17411 |
. . . . . 6
⊢
((doma‘(2nd ‘𝑧))(Homa‘𝐶)(coda‘(1st
‘𝑧))) ⊆ 𝐴 |
17 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ dom · → 𝑧 ∈ dom · ) |
18 | 11, 17 | eqeltrrd 2834 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ dom · →
〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ dom · ) |
19 | | df-br 5028 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑧)dom · (2nd
‘𝑧) ↔
〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ dom · ) |
20 | 18, 19 | sylibr 237 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ dom · →
(1st ‘𝑧)dom · (2nd
‘𝑧)) |
21 | 1, 2 | eldmcoa 17430 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧)dom · (2nd
‘𝑧) ↔
((2nd ‘𝑧)
∈ 𝐴 ∧
(1st ‘𝑧)
∈ 𝐴 ∧
(coda‘(2nd ‘𝑧)) =
(doma‘(1st ‘𝑧)))) |
22 | 20, 21 | sylib 221 |
. . . . . . . . . 10
⊢ (𝑧 ∈ dom · →
((2nd ‘𝑧)
∈ 𝐴 ∧
(1st ‘𝑧)
∈ 𝐴 ∧
(coda‘(2nd ‘𝑧)) =
(doma‘(1st ‘𝑧)))) |
23 | 22 | simp1d 1143 |
. . . . . . . . 9
⊢ (𝑧 ∈ dom · →
(2nd ‘𝑧)
∈ 𝐴) |
24 | 2, 15 | arwhoma 17410 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) ∈ 𝐴 → (2nd ‘𝑧) ∈
((doma‘(2nd ‘𝑧))(Homa‘𝐶)(coda‘(2nd
‘𝑧)))) |
25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ (𝑧 ∈ dom · →
(2nd ‘𝑧)
∈ ((doma‘(2nd ‘𝑧))(Homa‘𝐶)(coda‘(2nd
‘𝑧)))) |
26 | 22 | simp3d 1145 |
. . . . . . . . 9
⊢ (𝑧 ∈ dom · →
(coda‘(2nd ‘𝑧)) =
(doma‘(1st ‘𝑧))) |
27 | 26 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝑧 ∈ dom · →
((doma‘(2nd ‘𝑧))(Homa‘𝐶)(coda‘(2nd
‘𝑧))) =
((doma‘(2nd ‘𝑧))(Homa‘𝐶)(doma‘(1st
‘𝑧)))) |
28 | 25, 27 | eleqtrd 2835 |
. . . . . . 7
⊢ (𝑧 ∈ dom · →
(2nd ‘𝑧)
∈ ((doma‘(2nd ‘𝑧))(Homa‘𝐶)(doma‘(1st
‘𝑧)))) |
29 | 22 | simp2d 1144 |
. . . . . . . 8
⊢ (𝑧 ∈ dom · →
(1st ‘𝑧)
∈ 𝐴) |
30 | 2, 15 | arwhoma 17410 |
. . . . . . . 8
⊢
((1st ‘𝑧) ∈ 𝐴 → (1st ‘𝑧) ∈
((doma‘(1st ‘𝑧))(Homa‘𝐶)(coda‘(1st
‘𝑧)))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ dom · →
(1st ‘𝑧)
∈ ((doma‘(1st ‘𝑧))(Homa‘𝐶)(coda‘(1st
‘𝑧)))) |
32 | 1, 15, 28, 31 | coahom 17435 |
. . . . . 6
⊢ (𝑧 ∈ dom · →
((1st ‘𝑧)
·
(2nd ‘𝑧))
∈ ((doma‘(2nd ‘𝑧))(Homa‘𝐶)(coda‘(1st
‘𝑧)))) |
33 | 16, 32 | sseldi 3873 |
. . . . 5
⊢ (𝑧 ∈ dom · →
((1st ‘𝑧)
·
(2nd ‘𝑧))
∈ 𝐴) |
34 | 14, 33 | eqeltrd 2833 |
. . . 4
⊢ (𝑧 ∈ dom · → ( ·
‘𝑧) ∈ 𝐴) |
35 | 34 | rgen 3063 |
. . 3
⊢
∀𝑧 ∈ dom
·
( · ‘𝑧) ∈ 𝐴 |
36 | | ffnfv 6886 |
. . 3
⊢ ( · :dom
·
⟶𝐴 ↔ ( · Fn dom
·
∧ ∀𝑧 ∈ dom
·
( · ‘𝑧) ∈ 𝐴)) |
37 | 7, 35, 36 | mpbir2an 711 |
. 2
⊢ · :dom
·
⟶𝐴 |
38 | 2 | fvexi 6682 |
. . 3
⊢ 𝐴 ∈ V |
39 | 38, 38 | xpex 7488 |
. . 3
⊢ (𝐴 × 𝐴) ∈ V |
40 | 38, 39 | elpm2 8477 |
. 2
⊢ ( · ∈
(𝐴 ↑pm
(𝐴 × 𝐴)) ↔ ( · :dom ·
⟶𝐴 ∧ dom ·
⊆ (𝐴 × 𝐴))) |
41 | 37, 8, 40 | mpbir2an 711 |
1
⊢ · ∈
(𝐴 ↑pm
(𝐴 × 𝐴)) |