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 ⊢ 𝐵 = ( Base ‘ 𝐷 )
funcinv.s ⊢ 𝐼 = ( Inv ‘ 𝐷 )
funcinv.t ⊢ 𝐽 = ( Inv ‘ 𝐸 )
funcinv.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
funcinv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
funcinv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
funcinv.m ⊢ ( 𝜑 → 𝑀 ( 𝑋 𝐼 𝑌 ) 𝑁 )
Assertion funcinv ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 funcinv.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 funcinv.s ⊢ 𝐼 = ( Inv ‘ 𝐷 )
3 funcinv.t ⊢ 𝐽 = ( Inv ‘ 𝐸 )
4 funcinv.f ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5 funcinv.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 funcinv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 funcinv.m ⊢ ( 𝜑 → 𝑀 ( 𝑋 𝐼 𝑌 ) 𝑁 )
8 eqid ⊢ ( Sect ‘ 𝐷 ) = ( Sect ‘ 𝐷 )
9 eqid ⊢ ( Sect ‘ 𝐸 ) = ( Sect ‘ 𝐸 )
10 df-br ⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
11 4 10 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
12 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
13 11 12 syl ⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
14 13 simpld ⊢ ( 𝜑 → 𝐷 ∈ Cat )
15 1 2 14 5 6 8 isinv ⊢ ( 𝜑 → ( 𝑀 ( 𝑋 𝐼 𝑌 ) 𝑁 ↔ ( 𝑀 ( 𝑋 ( Sect ‘ 𝐷 ) 𝑌 ) 𝑁 ∧ 𝑁 ( 𝑌 ( Sect ‘ 𝐷 ) 𝑋 ) 𝑀 ) ) )
16 7 15 mpbid ⊢ ( 𝜑 → ( 𝑀 ( 𝑋 ( Sect ‘ 𝐷 ) 𝑌 ) 𝑁 ∧ 𝑁 ( 𝑌 ( Sect ‘ 𝐷 ) 𝑋 ) 𝑀 ) )
17 16 simpld ⊢ ( 𝜑 → 𝑀 ( 𝑋 ( Sect ‘ 𝐷 ) 𝑌 ) 𝑁 )
18 1 8 9 4 5 6 17 funcsect ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( Sect ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) )
19 16 simprd ⊢ ( 𝜑 → 𝑁 ( 𝑌 ( Sect ‘ 𝐷 ) 𝑋 ) 𝑀 )
20 1 8 9 4 6 5 19 funcsect ⊢ ( 𝜑 → ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑌 ) ( Sect ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) )
21 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
22 13 simprd ⊢ ( 𝜑 → 𝐸 ∈ Cat )
23 1 21 4 funcf1 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) )
24 23 5 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐸 ) )
25 23 6 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐸 ) )
26 21 3 22 24 25 9 isinv ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ↔ ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( Sect ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ∧ ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑌 ) ( Sect ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
27 18 20 26 mpbir2and ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) )