| Step | Hyp | Ref
| Expression |
| 1 | | coapm.o |
. . . . . 6
⊢ · =
(compa‘𝐶) |
| 2 | | coapm.a |
. . . . . 6
⊢ 𝐴 = (Arrow‘𝐶) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 4 | 1, 2, 3 | coafval 18109 |
. . . . 5
⊢ · =
(𝑔 ∈ 𝐴, 𝑓 ∈ {ℎ ∈ 𝐴 ∣ (coda‘ℎ) =
(doma‘𝑔)} ↦
〈(doma‘𝑓), (coda‘𝑔), ((2nd ‘𝑔)(〈(doma‘𝑓),
(doma‘𝑔)〉(comp‘𝐶)(coda‘𝑔))(2nd ‘𝑓))〉) |
| 5 | 4 | mpofun 7557 |
. . . 4
⊢ Fun · |
| 6 | | funfn 6596 |
. . . 4
⊢ (Fun
·
↔ · Fn dom ·
) |
| 7 | 5, 6 | mpbi 230 |
. . 3
⊢ · Fn dom
· |
| 8 | 1, 2 | dmcoass 18111 |
. . . . . . . . 9
⊢ dom ·
⊆ (𝐴 × 𝐴) |
| 9 | 8 | sseli 3979 |
. . . . . . . 8
⊢ (𝑧 ∈ dom · → 𝑧 ∈ (𝐴 × 𝐴)) |
| 10 | | 1st2nd2 8053 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 × 𝐴) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝑧 ∈ dom · → 𝑧 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
| 12 | 11 | fveq2d 6910 |
. . . . . 6
⊢ (𝑧 ∈ dom · → ( ·
‘𝑧) = ( ·
‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
| 13 | | df-ov 7434 |
. . . . . 6
⊢
((1st ‘𝑧) · (2nd
‘𝑧)) = ( ·
‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . 5
⊢ (𝑧 ∈ dom · → ( ·
‘𝑧) =
((1st ‘𝑧)
·
(2nd ‘𝑧))) |
| 15 | | eqid 2737 |
. . . . . . 7
⊢
(Homa‘𝐶) = (Homa‘𝐶) |
| 16 | 2, 15 | homarw 18091 |
. . . . . 6
⊢
((doma‘(2nd ‘𝑧))(Homa‘𝐶)(coda‘(1st
‘𝑧))) ⊆ 𝐴 |
| 17 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ dom · → 𝑧 ∈ dom · ) |
| 18 | 11, 17 | eqeltrrd 2842 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ dom · →
〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ dom · ) |
| 19 | | df-br 5144 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑧)dom · (2nd
‘𝑧) ↔
〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ dom · ) |
| 20 | 18, 19 | sylibr 234 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ dom · →
(1st ‘𝑧)dom · (2nd
‘𝑧)) |
| 21 | 1, 2 | eldmcoa 18110 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧)dom · (2nd
‘𝑧) ↔
((2nd ‘𝑧)
∈ 𝐴 ∧
(1st ‘𝑧)
∈ 𝐴 ∧
(coda‘(2nd ‘𝑧)) =
(doma‘(1st ‘𝑧)))) |
| 22 | 20, 21 | sylib 218 |
. . . . . . . . . 10
⊢ (𝑧 ∈ dom · →
((2nd ‘𝑧)
∈ 𝐴 ∧
(1st ‘𝑧)
∈ 𝐴 ∧
(coda‘(2nd ‘𝑧)) =
(doma‘(1st ‘𝑧)))) |
| 23 | 22 | simp1d 1143 |
. . . . . . . . 9
⊢ (𝑧 ∈ dom · →
(2nd ‘𝑧)
∈ 𝐴) |
| 24 | 2, 15 | arwhoma 18090 |
. . . . . . . . 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 7447 |
. . . . . . . 8
⊢ (𝑧 ∈ dom · →
((doma‘(2nd ‘𝑧))(Homa‘𝐶)(coda‘(2nd
‘𝑧))) =
((doma‘(2nd ‘𝑧))(Homa‘𝐶)(doma‘(1st
‘𝑧)))) |
| 28 | 25, 27 | eleqtrd 2843 |
. . . . . . 7
⊢ (𝑧 ∈ dom · →
(2nd ‘𝑧)
∈ ((doma‘(2nd ‘𝑧))(Homa‘𝐶)(doma‘(1st
‘𝑧)))) |
| 29 | 22 | simp2d 1144 |
. . . . . . . 8
⊢ (𝑧 ∈ dom · →
(1st ‘𝑧)
∈ 𝐴) |
| 30 | 2, 15 | arwhoma 18090 |
. . . . . . . 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 18115 |
. . . . . 6
⊢ (𝑧 ∈ dom · →
((1st ‘𝑧)
·
(2nd ‘𝑧))
∈ ((doma‘(2nd ‘𝑧))(Homa‘𝐶)(coda‘(1st
‘𝑧)))) |
| 33 | 16, 32 | sselid 3981 |
. . . . 5
⊢ (𝑧 ∈ dom · →
((1st ‘𝑧)
·
(2nd ‘𝑧))
∈ 𝐴) |
| 34 | 14, 33 | eqeltrd 2841 |
. . . 4
⊢ (𝑧 ∈ dom · → ( ·
‘𝑧) ∈ 𝐴) |
| 35 | 34 | rgen 3063 |
. . 3
⊢
∀𝑧 ∈ dom
·
( · ‘𝑧) ∈ 𝐴 |
| 36 | | ffnfv 7139 |
. . 3
⊢ ( · :dom
·
⟶𝐴 ↔ ( · Fn dom
·
∧ ∀𝑧 ∈ dom
·
( · ‘𝑧) ∈ 𝐴)) |
| 37 | 7, 35, 36 | mpbir2an 711 |
. 2
⊢ · :dom
·
⟶𝐴 |
| 38 | 2 | fvexi 6920 |
. . 3
⊢ 𝐴 ∈ V |
| 39 | 38, 38 | xpex 7773 |
. . 3
⊢ (𝐴 × 𝐴) ∈ V |
| 40 | 38, 39 | elpm2 8914 |
. 2
⊢ ( · ∈
(𝐴 ↑pm
(𝐴 × 𝐴)) ↔ ( · :dom ·
⟶𝐴 ∧ dom ·
⊆ (𝐴 × 𝐴))) |
| 41 | 37, 8, 40 | mpbir2an 711 |
1
⊢ · ∈
(𝐴 ↑pm
(𝐴 × 𝐴)) |