Metamath Proof Explorer

Theorem ffthiso

Description: A fully faithful functor reflects isomorphisms. Corollary 3.32 of Adamek p. 35. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
fthmon.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
fthmon.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
fthmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
fthmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
fthmon.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
ffthiso.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
ffthiso.s ⊢ 𝐼 = ( Iso ‘ 𝐶 )
ffthiso.t ⊢ 𝐽 = ( Iso ‘ 𝐷 )
Assertion ffthiso ( 𝜑 → ( 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 fthmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fthmon.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 fthmon.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
4 fthmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 fthmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 fthmon.r ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
7 ffthiso.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
8 ffthiso.s ⊢ 𝐼 = ( Iso ‘ 𝐶 )
9 ffthiso.t ⊢ 𝐽 = ( Iso ‘ 𝐷 )
10 fthfunc ⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
11 10 ssbri ⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
12 3 11 syl ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
14 4 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑋 ∈ 𝐵 )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑌 ∈ 𝐵 )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) )
17 1 8 9 13 14 15 16 funciso ⊢ ( ( 𝜑 ∧ 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
18 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
19 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
20 12 19 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
21 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
22 20 21 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
23 22 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
24 23 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → 𝐶 ∈ Cat )
25 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → 𝑋 ∈ 𝐵 )
26 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → 𝑌 ∈ 𝐵 )
27 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
28 eqid ⊢ ( Inv ‘ 𝐷 ) = ( Inv ‘ 𝐷 )
29 22 simprd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
30 1 27 12 funcf1 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
31 30 4 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
32 30 5 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
33 27 28 29 31 32 9 isoval ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) = dom ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
34 33 eleq2d ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ dom ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ) )
35 34 biimpa ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ dom ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
36 27 28 29 31 32 invfun ⊢ ( 𝜑 → Fun ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → Fun ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
38 funfvbrb ⊢ ( Fun ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ dom ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) ) )
39 37 38 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ dom ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) ) )
40 35 39 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) )
41 40 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) )
42 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) )
43 41 42 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) )
44 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
45 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → 𝑅 ∈ ( 𝑋 𝐻 𝑌 ) )
46 simplr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) )
47 1 2 44 25 26 45 46 18 28 fthinv ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → ( 𝑅 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) 𝑓 ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) )
48 43 47 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → 𝑅 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) 𝑓 )
49 1 18 24 25 26 8 48 inviso1 ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) ∧ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ) ∧ ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) ) → 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) )
50 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
51 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
52 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → 𝑌 ∈ 𝐵 )
53 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → 𝑋 ∈ 𝐵 )
54 27 50 9 29 32 31 isohom ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑌 ) 𝐽 ( 𝐹 ‘ 𝑋 ) ) ⊆ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → ( ( 𝐹 ‘ 𝑌 ) 𝐽 ( 𝐹 ‘ 𝑋 ) ) ⊆ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) )
56 27 28 29 31 32 9 invf ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) : ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ⟶ ( ( 𝐹 ‘ 𝑌 ) 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
57 56 ffvelcdmda ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) ∈ ( ( 𝐹 ‘ 𝑌 ) 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
58 55 57 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) ∈ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) )
59 1 50 2 51 52 53 58 fulli ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → ∃ 𝑓 ∈ ( 𝑌 𝐻 𝑋 ) ( ( ( 𝐹 ‘ 𝑋 ) ( Inv ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) ‘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ) = ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑓 ) )
60 49 59 r19.29a ⊢ ( ( 𝜑 ∧ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) → 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) )
61 17 60 impbida ⊢ ( 𝜑 → ( 𝑅 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑅 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )