Metamath Proof Explorer

Theorem catidex

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catidex.b ⊢B=BaseC
catidex.h ⊢H=Hom⁡C
catidex.o ⊢·˙=comp⁡C
catidex.c ⊢φ→C∈Cat
catidex.x ⊢φ→X∈B
Assertion catidex ⊢φ→∃g∈XHX∀y∈B∀f∈yHXgyX·˙Xf=f∧∀f∈XHyfXX·˙yg=f

Proof

Step Hyp Ref Expression
1 catidex.b ⊢B=BaseC
2 catidex.h ⊢H=Hom⁡C
3 catidex.o ⊢·˙=comp⁡C
4 catidex.c ⊢φ→C∈Cat
5 catidex.x ⊢φ→X∈B
6 id ⊢x=X→x=X
7 6 6 oveq12d ⊢x=X→xHx=XHX
8 oveq2 ⊢x=X→yHx=yHX
9 opeq2 ⊢x=X→yx=yX
10 9 6 oveq12d ⊢x=X→yx·˙x=yX·˙X
11 10 oveqd ⊢x=X→gyx·˙xf=gyX·˙Xf
12 11 eqeq1d ⊢x=X→gyx·˙xf=f↔gyX·˙Xf=f
13 8 12 raleqbidv ⊢x=X→∀f∈yHxgyx·˙xf=f↔∀f∈yHXgyX·˙Xf=f
14 oveq1 ⊢x=X→xHy=XHy
15 6 6 opeq12d ⊢x=X→xx=XX
16 15 oveq1d ⊢x=X→xx·˙y=XX·˙y
17 16 oveqd ⊢x=X→fxx·˙yg=fXX·˙yg
18 17 eqeq1d ⊢x=X→fxx·˙yg=f↔fXX·˙yg=f
19 14 18 raleqbidv ⊢x=X→∀f∈xHyfxx·˙yg=f↔∀f∈XHyfXX·˙yg=f
20 13 19 anbi12d ⊢x=X→∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f↔∀f∈yHXgyX·˙Xf=f∧∀f∈XHyfXX·˙yg=f
21 20 ralbidv ⊢x=X→∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f↔∀y∈B∀f∈yHXgyX·˙Xf=f∧∀f∈XHyfXX·˙yg=f
22 7 21 rexeqbidv ⊢x=X→∃g∈xHx∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f↔∃g∈XHX∀y∈B∀f∈yHXgyX·˙Xf=f∧∀f∈XHyfXX·˙yg=f
23 1 2 3 iscat ⊢C∈Cat→C∈Cat↔∀x∈B∃g∈xHx∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f∧∀y∈B∀z∈B∀f∈xHy∀g∈yHzgxy·˙zf∈xHz∧∀w∈B∀k∈zHwkyz·˙wgxy·˙wf=kxz·˙wgxy·˙zf
24 23 ibi ⊢C∈Cat→∀x∈B∃g∈xHx∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f∧∀y∈B∀z∈B∀f∈xHy∀g∈yHzgxy·˙zf∈xHz∧∀w∈B∀k∈zHwkyz·˙wgxy·˙wf=kxz·˙wgxy·˙zf
25 simpl ⊢∃g∈xHx∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f∧∀y∈B∀z∈B∀f∈xHy∀g∈yHzgxy·˙zf∈xHz∧∀w∈B∀k∈zHwkyz·˙wgxy·˙wf=kxz·˙wgxy·˙zf→∃g∈xHx∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f
26 25 ralimi ⊢∀x∈B∃g∈xHx∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f∧∀y∈B∀z∈B∀f∈xHy∀g∈yHzgxy·˙zf∈xHz∧∀w∈B∀k∈zHwkyz·˙wgxy·˙wf=kxz·˙wgxy·˙zf→∀x∈B∃g∈xHx∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f
27 4 24 26 3syl ⊢φ→∀x∈B∃g∈xHx∀y∈B∀f∈yHxgyx·˙xf=f∧∀f∈xHyfxx·˙yg=f
28 22 27 5 rspcdva ⊢φ→∃g∈XHX∀y∈B∀f∈yHXgyX·˙Xf=f∧∀f∈XHyfXX·˙yg=f