Metamath Proof Explorer

Theorem fthinv

Description: A faithful functor reflects inverses. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
fthsect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
fthsect.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
fthsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
fthsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
fthsect.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
fthsect.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐻 𝑋 ) )
fthinv.s ⊢ 𝐼 = ( Inv ‘ 𝐶 )
fthinv.t ⊢ 𝐽 = ( Inv ‘ 𝐷 )
Assertion fthinv ( 𝜑 → ( 𝑀 ( 𝑋 𝐼 𝑌 ) 𝑁 ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 fthsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fthsect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 fthsect.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
4 fthsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 fthsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 fthsect.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
7 fthsect.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐻 𝑋 ) )
8 fthinv.s ⊢ 𝐼 = ( Inv ‘ 𝐶 )
9 fthinv.t ⊢ 𝐽 = ( Inv ‘ 𝐷 )
10 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
11 eqid ⊢ ( Sect ‘ 𝐷 ) = ( Sect ‘ 𝐷 )
12 1 2 3 4 5 6 7 10 11 fthsect ⊢ ( 𝜑 → ( 𝑀 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑁 ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( Sect ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ) )
13 1 2 3 5 4 7 6 10 11 fthsect ⊢ ( 𝜑 → ( 𝑁 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝑀 ↔ ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑌 ) ( Sect ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) )
14 12 13 anbi12d ⊢ ( 𝜑 → ( ( 𝑀 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑁 ∧ 𝑁 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝑀 ) ↔ ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( Sect ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ∧ ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑌 ) ( Sect ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
15 fthfunc ⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
16 15 ssbri ⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
17 3 16 syl ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
18 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
19 17 18 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
20 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
21 19 20 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
22 21 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
23 1 8 22 4 5 10 isinv ⊢ ( 𝜑 → ( 𝑀 ( 𝑋 𝐼 𝑌 ) 𝑁 ↔ ( 𝑀 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝑁 ∧ 𝑁 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝑀 ) ) )
24 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
25 21 simprd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
26 1 24 17 funcf1 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
27 26 4 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
28 26 5 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
29 24 9 25 27 28 11 isinv ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ↔ ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) ( Sect ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ∧ ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ( 𝐹 ‘ 𝑌 ) ( Sect ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) ) )
30 14 23 29 3bitr4d ⊢ ( 𝜑 → ( 𝑀 ( 𝑋 𝐼 𝑌 ) 𝑁 ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ) )