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

Theorem isoval 16472
Description: The isomorphisms are the domain of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.) (Proof shortened by AV, 21-May-2020.)
Hypotheses
Ref Expression
invfval.b 𝐵 = (Base‘𝐶)
invfval.n 𝑁 = (Inv‘𝐶)
invfval.c (𝜑𝐶 ∈ Cat)
invfval.x (𝜑𝑋𝐵)
invfval.y (𝜑𝑌𝐵)
isoval.n 𝐼 = (Iso‘𝐶)
Assertion
Ref Expression
isoval (𝜑 → (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌))

Proof of Theorem isoval
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 invfval.c . . . . 5 (𝜑𝐶 ∈ Cat)
2 isofval 16464 . . . . 5 (𝐶 ∈ Cat → (Iso‘𝐶) = ((𝑧 ∈ V ↦ dom 𝑧) ∘ (Inv‘𝐶)))
31, 2syl 17 . . . 4 (𝜑 → (Iso‘𝐶) = ((𝑧 ∈ V ↦ dom 𝑧) ∘ (Inv‘𝐶)))
4 isoval.n . . . 4 𝐼 = (Iso‘𝐶)
5 invfval.n . . . . 5 𝑁 = (Inv‘𝐶)
65coeq2i 5315 . . . 4 ((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁) = ((𝑧 ∈ V ↦ dom 𝑧) ∘ (Inv‘𝐶))
73, 4, 63eqtr4g 2710 . . 3 (𝜑𝐼 = ((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁))
87oveqd 6707 . 2 (𝜑 → (𝑋𝐼𝑌) = (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌))
9 eqid 2651 . . . . . 6 (𝑥𝐵, 𝑦𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ (𝑦(Sect‘𝐶)𝑥))) = (𝑥𝐵, 𝑦𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ (𝑦(Sect‘𝐶)𝑥)))
10 ovex 6718 . . . . . . 7 (𝑥(Sect‘𝐶)𝑦) ∈ V
1110inex1 4832 . . . . . 6 ((𝑥(Sect‘𝐶)𝑦) ∩ (𝑦(Sect‘𝐶)𝑥)) ∈ V
129, 11fnmpt2i 7284 . . . . 5 (𝑥𝐵, 𝑦𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ (𝑦(Sect‘𝐶)𝑥))) Fn (𝐵 × 𝐵)
13 invfval.b . . . . . . 7 𝐵 = (Base‘𝐶)
14 invfval.x . . . . . . 7 (𝜑𝑋𝐵)
15 invfval.y . . . . . . 7 (𝜑𝑌𝐵)
16 eqid 2651 . . . . . . 7 (Sect‘𝐶) = (Sect‘𝐶)
1713, 5, 1, 14, 15, 16invffval 16465 . . . . . 6 (𝜑𝑁 = (𝑥𝐵, 𝑦𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ (𝑦(Sect‘𝐶)𝑥))))
1817fneq1d 6019 . . . . 5 (𝜑 → (𝑁 Fn (𝐵 × 𝐵) ↔ (𝑥𝐵, 𝑦𝐵 ↦ ((𝑥(Sect‘𝐶)𝑦) ∩ (𝑦(Sect‘𝐶)𝑥))) Fn (𝐵 × 𝐵)))
1912, 18mpbiri 248 . . . 4 (𝜑𝑁 Fn (𝐵 × 𝐵))
20 opelxpi 5182 . . . . 5 ((𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
2114, 15, 20syl2anc 694 . . . 4 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵))
22 fvco2 6312 . . . 4 ((𝑁 Fn (𝐵 × 𝐵) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵)) → (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘⟨𝑋, 𝑌⟩) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘⟨𝑋, 𝑌⟩)))
2319, 21, 22syl2anc 694 . . 3 (𝜑 → (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘⟨𝑋, 𝑌⟩) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘⟨𝑋, 𝑌⟩)))
24 df-ov 6693 . . 3 (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌) = (((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)‘⟨𝑋, 𝑌⟩)
25 ovex 6718 . . . . 5 (𝑋𝑁𝑌) ∈ V
26 dmeq 5356 . . . . . 6 (𝑧 = (𝑋𝑁𝑌) → dom 𝑧 = dom (𝑋𝑁𝑌))
27 eqid 2651 . . . . . 6 (𝑧 ∈ V ↦ dom 𝑧) = (𝑧 ∈ V ↦ dom 𝑧)
2825dmex 7141 . . . . . 6 dom (𝑋𝑁𝑌) ∈ V
2926, 27, 28fvmpt 6321 . . . . 5 ((𝑋𝑁𝑌) ∈ V → ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = dom (𝑋𝑁𝑌))
3025, 29ax-mp 5 . . . 4 ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = dom (𝑋𝑁𝑌)
31 df-ov 6693 . . . . 5 (𝑋𝑁𝑌) = (𝑁‘⟨𝑋, 𝑌⟩)
3231fveq2i 6232 . . . 4 ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑋𝑁𝑌)) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘⟨𝑋, 𝑌⟩))
3330, 32eqtr3i 2675 . . 3 dom (𝑋𝑁𝑌) = ((𝑧 ∈ V ↦ dom 𝑧)‘(𝑁‘⟨𝑋, 𝑌⟩))
3423, 24, 333eqtr4g 2710 . 2 (𝜑 → (𝑋((𝑧 ∈ V ↦ dom 𝑧) ∘ 𝑁)𝑌) = dom (𝑋𝑁𝑌))
358, 34eqtrd 2685 1 (𝜑 → (𝑋𝐼𝑌) = dom (𝑋𝑁𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  Vcvv 3231  cin 3606  cop 4216  cmpt 4762   × cxp 5141  ccnv 5142  dom cdm 5143  ccom 5147   Fn wfn 5921  cfv 5926  (class class class)co 6690  cmpt2 6692  Basecbs 15904  Catccat 16372  Sectcsect 16451  Invcinv 16452  Isociso 16453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-inv 16455  df-iso 16456
This theorem is referenced by:  inviso1  16473  invf  16475  invco  16478  dfiso2  16479  isohom  16483  oppciso  16488  cicsym  16511  funciso  16581  ffthiso  16636  fuciso  16682  setciso  16788  catciso  16804  rngciso  42307  rngcisoALTV  42319  ringciso  42358  ringcisoALTV  42382
  Copyright terms: Public domain W3C validator