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

Theorem isocnv 6771
Description: Converse law for isomorphism. Proposition 6.30(2) of [TakeutiZaring] p. 33. (Contributed by NM, 27-Apr-2004.)
Assertion
Ref Expression
isocnv (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))

Proof of Theorem isocnv
Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1ocnv 6331 . . . 4 (𝐻:𝐴1-1-onto𝐵𝐻:𝐵1-1-onto𝐴)
21adantr 472 . . 3 ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → 𝐻:𝐵1-1-onto𝐴)
3 f1ocnvfv2 6724 . . . . . . . 8 ((𝐻:𝐴1-1-onto𝐵𝑧𝐵) → (𝐻‘(𝐻𝑧)) = 𝑧)
43adantrr 708 . . . . . . 7 ((𝐻:𝐴1-1-onto𝐵 ∧ (𝑧𝐵𝑤𝐵)) → (𝐻‘(𝐻𝑧)) = 𝑧)
5 f1ocnvfv2 6724 . . . . . . . 8 ((𝐻:𝐴1-1-onto𝐵𝑤𝐵) → (𝐻‘(𝐻𝑤)) = 𝑤)
65adantrl 707 . . . . . . 7 ((𝐻:𝐴1-1-onto𝐵 ∧ (𝑧𝐵𝑤𝐵)) → (𝐻‘(𝐻𝑤)) = 𝑤)
74, 6breq12d 4821 . . . . . 6 ((𝐻:𝐴1-1-onto𝐵 ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ 𝑧𝑆𝑤))
87adantlr 706 . . . . 5 (((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ 𝑧𝑆𝑤))
9 f1of 6319 . . . . . . 7 (𝐻:𝐵1-1-onto𝐴𝐻:𝐵𝐴)
101, 9syl 17 . . . . . 6 (𝐻:𝐴1-1-onto𝐵𝐻:𝐵𝐴)
11 ffvelrn 6546 . . . . . . . . 9 ((𝐻:𝐵𝐴𝑧𝐵) → (𝐻𝑧) ∈ 𝐴)
12 ffvelrn 6546 . . . . . . . . 9 ((𝐻:𝐵𝐴𝑤𝐵) → (𝐻𝑤) ∈ 𝐴)
1311, 12anim12dan 612 . . . . . . . 8 ((𝐻:𝐵𝐴 ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻𝑧) ∈ 𝐴 ∧ (𝐻𝑤) ∈ 𝐴))
14 breq1 4811 . . . . . . . . . . 11 (𝑥 = (𝐻𝑧) → (𝑥𝑅𝑦 ↔ (𝐻𝑧)𝑅𝑦))
15 fveq2 6374 . . . . . . . . . . . 12 (𝑥 = (𝐻𝑧) → (𝐻𝑥) = (𝐻‘(𝐻𝑧)))
1615breq1d 4818 . . . . . . . . . . 11 (𝑥 = (𝐻𝑧) → ((𝐻𝑥)𝑆(𝐻𝑦) ↔ (𝐻‘(𝐻𝑧))𝑆(𝐻𝑦)))
1714, 16bibi12d 336 . . . . . . . . . 10 (𝑥 = (𝐻𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ((𝐻𝑧)𝑅𝑦 ↔ (𝐻‘(𝐻𝑧))𝑆(𝐻𝑦))))
18 bicom 213 . . . . . . . . . 10 (((𝐻𝑧)𝑅𝑦 ↔ (𝐻‘(𝐻𝑧))𝑆(𝐻𝑦)) ↔ ((𝐻‘(𝐻𝑧))𝑆(𝐻𝑦) ↔ (𝐻𝑧)𝑅𝑦))
1917, 18syl6bb 278 . . . . . . . . 9 (𝑥 = (𝐻𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ((𝐻‘(𝐻𝑧))𝑆(𝐻𝑦) ↔ (𝐻𝑧)𝑅𝑦)))
20 fveq2 6374 . . . . . . . . . . 11 (𝑦 = (𝐻𝑤) → (𝐻𝑦) = (𝐻‘(𝐻𝑤)))
2120breq2d 4820 . . . . . . . . . 10 (𝑦 = (𝐻𝑤) → ((𝐻‘(𝐻𝑧))𝑆(𝐻𝑦) ↔ (𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤))))
22 breq2 4812 . . . . . . . . . 10 (𝑦 = (𝐻𝑤) → ((𝐻𝑧)𝑅𝑦 ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2321, 22bibi12d 336 . . . . . . . . 9 (𝑦 = (𝐻𝑤) → (((𝐻‘(𝐻𝑧))𝑆(𝐻𝑦) ↔ (𝐻𝑧)𝑅𝑦) ↔ ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤))))
2419, 23rspc2va 3474 . . . . . . . 8 ((((𝐻𝑧) ∈ 𝐴 ∧ (𝐻𝑤) ∈ 𝐴) ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2513, 24sylan 575 . . . . . . 7 (((𝐻:𝐵𝐴 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2625an32s 642 . . . . . 6 (((𝐻:𝐵𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2710, 26sylanl1 670 . . . . 5 (((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
288, 27bitr3d 272 . . . 4 (((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧𝑆𝑤 ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2928ralrimivva 3117 . . 3 ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → ∀𝑧𝐵𝑤𝐵 (𝑧𝑆𝑤 ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
302, 29jca 507 . 2 ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → (𝐻:𝐵1-1-onto𝐴 ∧ ∀𝑧𝐵𝑤𝐵 (𝑧𝑆𝑤 ↔ (𝐻𝑧)𝑅(𝐻𝑤))))
31 df-isom 6076 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
32 df-isom 6076 . 2 (𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴) ↔ (𝐻:𝐵1-1-onto𝐴 ∧ ∀𝑧𝐵𝑤𝐵 (𝑧𝑆𝑤 ↔ (𝐻𝑧)𝑅(𝐻𝑤))))
3330, 31, 323imtr4i 283 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3054   class class class wbr 4808  ccnv 5275  wf 6063  1-1-ontowf1o 6066  cfv 6067   Isom wiso 6068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-sbc 3596  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-br 4809  df-opab 4871  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076
This theorem is referenced by:  isores1  6775  isofr  6783  isose  6784  isopo  6787  isoso  6789  weisoeq  6796  weisoeq2  6797  fnwelem  7493  oieu  8650  oemapwe  8805  cantnffval2  8806  wemapwe  8808  infxpenlem  9086  fpwwe2lem7  9710  fpwwe2lem9  9712  infrenegsup  11259  ltweuz  12967  fz1isolem  13445  ordthmeo  21884  relogiso  24634  erdsze2lem2  31565  fzisoeu  40085
  Copyright terms: Public domain W3C validator