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

Theorem dfiso3 17032
Description: Alternate definition of an isomorphism of a category as a section in both directions. (Contributed by AV, 11-Apr-2020.)
Hypotheses
Ref Expression
dfiso3.b 𝐵 = (Base‘𝐶)
dfiso3.h 𝐻 = (Hom ‘𝐶)
dfiso3.i 𝐼 = (Iso‘𝐶)
dfiso3.s 𝑆 = (Sect‘𝐶)
dfiso3.c (𝜑𝐶 ∈ Cat)
dfiso3.x (𝜑𝑋𝐵)
dfiso3.y (𝜑𝑌𝐵)
dfiso3.f (𝜑𝐹 ∈ (𝑋𝐻𝑌))
Assertion
Ref Expression
dfiso3 (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)(𝑔(𝑌𝑆𝑋)𝐹𝐹(𝑋𝑆𝑌)𝑔)))
Distinct variable groups:   𝐶,𝑔   𝑔,𝐹   𝑔,𝐻   𝑔,𝐼   𝑔,𝑋   𝑔,𝑌   𝜑,𝑔
Allowed substitution hints:   𝐵(𝑔)   𝑆(𝑔)

Proof of Theorem dfiso3
StepHypRef Expression
1 dfiso3.b . . 3 𝐵 = (Base‘𝐶)
2 dfiso3.h . . 3 𝐻 = (Hom ‘𝐶)
3 dfiso3.c . . 3 (𝜑𝐶 ∈ Cat)
4 dfiso3.i . . 3 𝐼 = (Iso‘𝐶)
5 dfiso3.x . . 3 (𝜑𝑋𝐵)
6 dfiso3.y . . 3 (𝜑𝑌𝐵)
7 dfiso3.f . . 3 (𝜑𝐹 ∈ (𝑋𝐻𝑌))
8 eqid 2824 . . 3 (Id‘𝐶) = (Id‘𝐶)
9 eqid 2824 . . 3 (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋) = (⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)
10 eqid 2824 . . 3 (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌) = (⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)
111, 2, 3, 4, 5, 6, 7, 8, 9, 10dfiso2 17031 . 2 (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ((Id‘𝐶)‘𝑌))))
12 eqid 2824 . . . . . 6 (comp‘𝐶) = (comp‘𝐶)
13 dfiso3.s . . . . . 6 𝑆 = (Sect‘𝐶)
143adantr 484 . . . . . 6 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → 𝐶 ∈ Cat)
156adantr 484 . . . . . 6 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → 𝑌𝐵)
165adantr 484 . . . . . 6 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → 𝑋𝐵)
17 simpr 488 . . . . . 6 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → 𝑔 ∈ (𝑌𝐻𝑋))
187adantr 484 . . . . . 6 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → 𝐹 ∈ (𝑋𝐻𝑌))
191, 2, 12, 8, 13, 14, 15, 16, 17, 18issect2 17013 . . . . 5 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → (𝑔(𝑌𝑆𝑋)𝐹 ↔ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ((Id‘𝐶)‘𝑌)))
201, 2, 12, 8, 13, 14, 16, 15, 18, 17issect2 17013 . . . . 5 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → (𝐹(𝑋𝑆𝑌)𝑔 ↔ (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))
2119, 20anbi12d 633 . . . 4 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → ((𝑔(𝑌𝑆𝑋)𝐹𝐹(𝑋𝑆𝑌)𝑔) ↔ ((𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ((Id‘𝐶)‘𝑌) ∧ (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))))
22 ancom 464 . . . 4 (((𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ((Id‘𝐶)‘𝑌) ∧ (𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) ↔ ((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ((Id‘𝐶)‘𝑌)))
2321, 22syl6rbb 291 . . 3 ((𝜑𝑔 ∈ (𝑌𝐻𝑋)) → (((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ((Id‘𝐶)‘𝑌)) ↔ (𝑔(𝑌𝑆𝑋)𝐹𝐹(𝑋𝑆𝑌)𝑔)))
2423rexbidva 3288 . 2 (𝜑 → (∃𝑔 ∈ (𝑌𝐻𝑋)((𝑔(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)𝑔) = ((Id‘𝐶)‘𝑌)) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)(𝑔(𝑌𝑆𝑋)𝐹𝐹(𝑋𝑆𝑌)𝑔)))
2511, 24bitrd 282 1 (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ ∃𝑔 ∈ (𝑌𝐻𝑋)(𝑔(𝑌𝑆𝑋)𝐹𝐹(𝑋𝑆𝑌)𝑔)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wrex 3133  cop 4554   class class class wbr 5047  cfv 6336  (class class class)co 7138  Basecbs 16472  Hom chom 16565  compcco 16566  Catccat 16924  Idccid 16925  Sectcsect 17003  Isociso 17005
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-reu 3139  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7141  df-oprab 7142  df-mpo 7143  df-1st 7672  df-2nd 7673  df-sect 17006  df-inv 17007  df-iso 17008
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator