MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffthiso Structured version   Visualization version   GIF version

Theorem ffthiso 17816
Description: A fully faithful functor reflects isomorphisms. Corollary 3.32 of [Adamek] p. 35. (Contributed by Mario Carneiro, 27-Jan-2017.)
Hypotheses
Ref Expression
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
Ref Expression
ffthiso (𝜑 → (𝑅 ∈ (𝑋𝐼𝑌) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))))

Proof of Theorem ffthiso
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 fthmon.b . . 3 𝐵 = (Base‘𝐶)
2 ffthiso.s . . 3 𝐼 = (Iso‘𝐶)
3 ffthiso.t . . 3 𝐽 = (Iso‘𝐷)
4 fthmon.f . . . . 5 (𝜑𝐹(𝐶 Faith 𝐷)𝐺)
5 fthfunc 17794 . . . . . 6 (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷)
65ssbri 5150 . . . . 5 (𝐹(𝐶 Faith 𝐷)𝐺𝐹(𝐶 Func 𝐷)𝐺)
74, 6syl 17 . . . 4 (𝜑𝐹(𝐶 Func 𝐷)𝐺)
87adantr 481 . . 3 ((𝜑𝑅 ∈ (𝑋𝐼𝑌)) → 𝐹(𝐶 Func 𝐷)𝐺)
9 fthmon.x . . . 4 (𝜑𝑋𝐵)
109adantr 481 . . 3 ((𝜑𝑅 ∈ (𝑋𝐼𝑌)) → 𝑋𝐵)
11 fthmon.y . . . 4 (𝜑𝑌𝐵)
1211adantr 481 . . 3 ((𝜑𝑅 ∈ (𝑋𝐼𝑌)) → 𝑌𝐵)
13 simpr 485 . . 3 ((𝜑𝑅 ∈ (𝑋𝐼𝑌)) → 𝑅 ∈ (𝑋𝐼𝑌))
141, 2, 3, 8, 10, 12, 13funciso 17760 . 2 ((𝜑𝑅 ∈ (𝑋𝐼𝑌)) → ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌)))
15 eqid 2736 . . . 4 (Inv‘𝐶) = (Inv‘𝐶)
16 df-br 5106 . . . . . . . 8 (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
177, 16sylib 217 . . . . . . 7 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
18 funcrcl 17749 . . . . . . 7 (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
1917, 18syl 17 . . . . . 6 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
2019simpld 495 . . . . 5 (𝜑𝐶 ∈ Cat)
2120ad3antrrr 728 . . . 4 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝐶 ∈ Cat)
229ad3antrrr 728 . . . 4 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑋𝐵)
2311ad3antrrr 728 . . . 4 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑌𝐵)
24 eqid 2736 . . . . . . . . . . 11 (Base‘𝐷) = (Base‘𝐷)
25 eqid 2736 . . . . . . . . . . 11 (Inv‘𝐷) = (Inv‘𝐷)
2619simprd 496 . . . . . . . . . . 11 (𝜑𝐷 ∈ Cat)
271, 24, 7funcf1 17752 . . . . . . . . . . . 12 (𝜑𝐹:𝐵⟶(Base‘𝐷))
2827, 9ffvelcdmd 7036 . . . . . . . . . . 11 (𝜑 → (𝐹𝑋) ∈ (Base‘𝐷))
2927, 11ffvelcdmd 7036 . . . . . . . . . . 11 (𝜑 → (𝐹𝑌) ∈ (Base‘𝐷))
3024, 25, 26, 28, 29, 3isoval 17648 . . . . . . . . . 10 (𝜑 → ((𝐹𝑋)𝐽(𝐹𝑌)) = dom ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌)))
3130eleq2d 2823 . . . . . . . . 9 (𝜑 → (((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))))
3231biimpa 477 . . . . . . . 8 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → ((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌)))
3324, 25, 26, 28, 29invfun 17647 . . . . . . . . . 10 (𝜑 → Fun ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌)))
3433adantr 481 . . . . . . . . 9 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → Fun ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌)))
35 funfvbrb 7001 . . . . . . . . 9 (Fun ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌)) → (((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))(((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅))))
3634, 35syl 17 . . . . . . . 8 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → (((𝑋𝐺𝑌)‘𝑅) ∈ dom ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌)) ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))(((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅))))
3732, 36mpbid 231 . . . . . . 7 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → ((𝑋𝐺𝑌)‘𝑅)((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))(((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)))
3837ad2antrr 724 . . . . . 6 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → ((𝑋𝐺𝑌)‘𝑅)((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))(((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)))
39 simpr 485 . . . . . 6 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓))
4038, 39breqtrd 5131 . . . . 5 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → ((𝑋𝐺𝑌)‘𝑅)((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))((𝑌𝐺𝑋)‘𝑓))
41 fthmon.h . . . . . 6 𝐻 = (Hom ‘𝐶)
424ad3antrrr 728 . . . . . 6 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝐹(𝐶 Faith 𝐷)𝐺)
43 fthmon.r . . . . . . 7 (𝜑𝑅 ∈ (𝑋𝐻𝑌))
4443ad3antrrr 728 . . . . . 6 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅 ∈ (𝑋𝐻𝑌))
45 simplr 767 . . . . . 6 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑓 ∈ (𝑌𝐻𝑋))
461, 41, 42, 22, 23, 44, 45, 15, 25fthinv 17813 . . . . 5 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → (𝑅(𝑋(Inv‘𝐶)𝑌)𝑓 ↔ ((𝑋𝐺𝑌)‘𝑅)((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))((𝑌𝐺𝑋)‘𝑓)))
4740, 46mpbird 256 . . . 4 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅(𝑋(Inv‘𝐶)𝑌)𝑓)
481, 15, 21, 22, 23, 2, 47inviso1 17649 . . 3 ((((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) ∧ 𝑓 ∈ (𝑌𝐻𝑋)) ∧ (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓)) → 𝑅 ∈ (𝑋𝐼𝑌))
49 eqid 2736 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
50 ffthiso.f . . . . 5 (𝜑𝐹(𝐶 Full 𝐷)𝐺)
5150adantr 481 . . . 4 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → 𝐹(𝐶 Full 𝐷)𝐺)
5211adantr 481 . . . 4 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → 𝑌𝐵)
539adantr 481 . . . 4 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → 𝑋𝐵)
5424, 49, 3, 26, 29, 28isohom 17659 . . . . . 6 (𝜑 → ((𝐹𝑌)𝐽(𝐹𝑋)) ⊆ ((𝐹𝑌)(Hom ‘𝐷)(𝐹𝑋)))
5554adantr 481 . . . . 5 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → ((𝐹𝑌)𝐽(𝐹𝑋)) ⊆ ((𝐹𝑌)(Hom ‘𝐷)(𝐹𝑋)))
5624, 25, 26, 28, 29, 3invf 17651 . . . . . 6 (𝜑 → ((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌)):((𝐹𝑋)𝐽(𝐹𝑌))⟶((𝐹𝑌)𝐽(𝐹𝑋)))
5756ffvelcdmda 7035 . . . . 5 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) ∈ ((𝐹𝑌)𝐽(𝐹𝑋)))
5855, 57sseldd 3945 . . . 4 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → (((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) ∈ ((𝐹𝑌)(Hom ‘𝐷)(𝐹𝑋)))
591, 49, 41, 51, 52, 53, 58fulli 17800 . . 3 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → ∃𝑓 ∈ (𝑌𝐻𝑋)(((𝐹𝑋)(Inv‘𝐷)(𝐹𝑌))‘((𝑋𝐺𝑌)‘𝑅)) = ((𝑌𝐺𝑋)‘𝑓))
6048, 59r19.29a 3159 . 2 ((𝜑 ∧ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))) → 𝑅 ∈ (𝑋𝐼𝑌))
6114, 60impbida 799 1 (𝜑 → (𝑅 ∈ (𝑋𝐼𝑌) ↔ ((𝑋𝐺𝑌)‘𝑅) ∈ ((𝐹𝑋)𝐽(𝐹𝑌))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wss 3910  cop 4592   class class class wbr 5105  dom cdm 5633  Fun wfun 6490  cfv 6496  (class class class)co 7357  Basecbs 17083  Hom chom 17144  Catccat 17544  Invcinv 17628  Isociso 17629   Func cfunc 17740   Full cful 17789   Faith cfth 17790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767  df-ixp 8836  df-cat 17548  df-cid 17549  df-sect 17630  df-inv 17631  df-iso 17632  df-func 17744  df-full 17791  df-fth 17792
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator