Metamath Proof Explorer

Theorem funcinv

Description: The image of an inverse under a functor is an inverse. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses funcinv.b ⊢B=BaseD
funcinv.s ⊢I=Inv⁡D
funcinv.t ⊢J=Inv⁡E
funcinv.f ⊢φ→FDFuncEG
funcinv.x ⊢φ→X∈B
funcinv.y ⊢φ→Y∈B
funcinv.m ⊢φ→MXIYN
Assertion funcinv ⊢φ→XGY⁡MF⁡XJF⁡YYGX⁡N

Proof

Step Hyp Ref Expression
1 funcinv.b ⊢B=BaseD
2 funcinv.s ⊢I=Inv⁡D
3 funcinv.t ⊢J=Inv⁡E
4 funcinv.f ⊢φ→FDFuncEG
5 funcinv.x ⊢φ→X∈B
6 funcinv.y ⊢φ→Y∈B
7 funcinv.m ⊢φ→MXIYN
8 eqid ⊢Sect⁡D=Sect⁡D
9 eqid ⊢Sect⁡E=Sect⁡E
10 df-br ⊢FDFuncEG↔FG∈DFuncE
11 4 10 sylib ⊢φ→FG∈DFuncE
12 funcrcl ⊢FG∈DFuncE→D∈Cat∧E∈Cat
13 11 12 syl ⊢φ→D∈Cat∧E∈Cat
14 13 simpld ⊢φ→D∈Cat
15 1 2 14 5 6 8 isinv ⊢φ→MXIYN↔MXSect⁡DYN∧NYSect⁡DXM
16 7 15 mpbid ⊢φ→MXSect⁡DYN∧NYSect⁡DXM
17 16 simpld ⊢φ→MXSect⁡DYN
18 1 8 9 4 5 6 17 funcsect ⊢φ→XGY⁡MF⁡XSect⁡EF⁡YYGX⁡N
19 16 simprd ⊢φ→NYSect⁡DXM
20 1 8 9 4 6 5 19 funcsect ⊢φ→YGX⁡NF⁡YSect⁡EF⁡XXGY⁡M
21 eqid ⊢BaseE=BaseE
22 13 simprd ⊢φ→E∈Cat
23 1 21 4 funcf1 ⊢φ→F:B⟶BaseE
24 23 5 ffvelcdmd ⊢φ→F⁡X∈BaseE
25 23 6 ffvelcdmd ⊢φ→F⁡Y∈BaseE
26 21 3 22 24 25 9 isinv ⊢φ→XGY⁡MF⁡XJF⁡YYGX⁡N↔XGY⁡MF⁡XSect⁡EF⁡YYGX⁡N∧YGX⁡NF⁡YSect⁡EF⁡XXGY⁡M
27 18 20 26 mpbir2and ⊢φ→XGY⁡MF⁡XJF⁡YYGX⁡N