Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  isocnv GIF version

Theorem isocnv 5721
 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 5389 . . . 4 (𝐻:𝐴1-1-onto𝐵𝐻:𝐵1-1-onto𝐴)
21adantr 274 . . 3 ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → 𝐻:𝐵1-1-onto𝐴)
3 f1ocnvfv2 5688 . . . . . . . 8 ((𝐻:𝐴1-1-onto𝐵𝑧𝐵) → (𝐻‘(𝐻𝑧)) = 𝑧)
43adantrr 471 . . . . . . 7 ((𝐻:𝐴1-1-onto𝐵 ∧ (𝑧𝐵𝑤𝐵)) → (𝐻‘(𝐻𝑧)) = 𝑧)
5 f1ocnvfv2 5688 . . . . . . . 8 ((𝐻:𝐴1-1-onto𝐵𝑤𝐵) → (𝐻‘(𝐻𝑤)) = 𝑤)
65adantrl 470 . . . . . . 7 ((𝐻:𝐴1-1-onto𝐵 ∧ (𝑧𝐵𝑤𝐵)) → (𝐻‘(𝐻𝑤)) = 𝑤)
74, 6breq12d 3951 . . . . . 6 ((𝐻:𝐴1-1-onto𝐵 ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ 𝑧𝑆𝑤))
87adantlr 469 . . . . 5 (((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ 𝑧𝑆𝑤))
9 f1of 5376 . . . . . . 7 (𝐻:𝐵1-1-onto𝐴𝐻:𝐵𝐴)
101, 9syl 14 . . . . . 6 (𝐻:𝐴1-1-onto𝐵𝐻:𝐵𝐴)
11 ffvelrn 5562 . . . . . . . . 9 ((𝐻:𝐵𝐴𝑧𝐵) → (𝐻𝑧) ∈ 𝐴)
12 ffvelrn 5562 . . . . . . . . 9 ((𝐻:𝐵𝐴𝑤𝐵) → (𝐻𝑤) ∈ 𝐴)
1311, 12anim12dan 590 . . . . . . . 8 ((𝐻:𝐵𝐴 ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻𝑧) ∈ 𝐴 ∧ (𝐻𝑤) ∈ 𝐴))
14 breq1 3941 . . . . . . . . . . 11 (𝑥 = (𝐻𝑧) → (𝑥𝑅𝑦 ↔ (𝐻𝑧)𝑅𝑦))
15 fveq2 5430 . . . . . . . . . . . 12 (𝑥 = (𝐻𝑧) → (𝐻𝑥) = (𝐻‘(𝐻𝑧)))
1615breq1d 3948 . . . . . . . . . . 11 (𝑥 = (𝐻𝑧) → ((𝐻𝑥)𝑆(𝐻𝑦) ↔ (𝐻‘(𝐻𝑧))𝑆(𝐻𝑦)))
1714, 16bibi12d 234 . . . . . . . . . 10 (𝑥 = (𝐻𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ((𝐻𝑧)𝑅𝑦 ↔ (𝐻‘(𝐻𝑧))𝑆(𝐻𝑦))))
18 bicom 139 . . . . . . . . . 10 (((𝐻𝑧)𝑅𝑦 ↔ (𝐻‘(𝐻𝑧))𝑆(𝐻𝑦)) ↔ ((𝐻‘(𝐻𝑧))𝑆(𝐻𝑦) ↔ (𝐻𝑧)𝑅𝑦))
1917, 18syl6bb 195 . . . . . . . . 9 (𝑥 = (𝐻𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ((𝐻‘(𝐻𝑧))𝑆(𝐻𝑦) ↔ (𝐻𝑧)𝑅𝑦)))
20 fveq2 5430 . . . . . . . . . . 11 (𝑦 = (𝐻𝑤) → (𝐻𝑦) = (𝐻‘(𝐻𝑤)))
2120breq2d 3950 . . . . . . . . . 10 (𝑦 = (𝐻𝑤) → ((𝐻‘(𝐻𝑧))𝑆(𝐻𝑦) ↔ (𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤))))
22 breq2 3942 . . . . . . . . . 10 (𝑦 = (𝐻𝑤) → ((𝐻𝑧)𝑅𝑦 ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2321, 22bibi12d 234 . . . . . . . . 9 (𝑦 = (𝐻𝑤) → (((𝐻‘(𝐻𝑧))𝑆(𝐻𝑦) ↔ (𝐻𝑧)𝑅𝑦) ↔ ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤))))
2419, 23rspc2va 2808 . . . . . . . 8 ((((𝐻𝑧) ∈ 𝐴 ∧ (𝐻𝑤) ∈ 𝐴) ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2513, 24sylan 281 . . . . . . 7 (((𝐻:𝐵𝐴 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2625an32s 558 . . . . . 6 (((𝐻:𝐵𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2710, 26sylanl1 400 . . . . 5 (((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ∧ (𝑧𝐵𝑤𝐵)) → ((𝐻‘(𝐻𝑧))𝑆(𝐻‘(𝐻𝑤)) ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
288, 27bitr3d 189 . . . 4 (((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ∧ (𝑧𝐵𝑤𝐵)) → (𝑧𝑆𝑤 ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
2928ralrimivva 2518 . . 3 ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → ∀𝑧𝐵𝑤𝐵 (𝑧𝑆𝑤 ↔ (𝐻𝑧)𝑅(𝐻𝑤)))
302, 29jca 304 . 2 ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) → (𝐻:𝐵1-1-onto𝐴 ∧ ∀𝑧𝐵𝑤𝐵 (𝑧𝑆𝑤 ↔ (𝐻𝑧)𝑅(𝐻𝑤))))
31 df-isom 5141 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
32 df-isom 5141 . 2 (𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴) ↔ (𝐻:𝐵1-1-onto𝐴 ∧ ∀𝑧𝐵𝑤𝐵 (𝑧𝑆𝑤 ↔ (𝐻𝑧)𝑅(𝐻𝑤))))
3330, 31, 323imtr4i 200 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  ∀wral 2417   class class class wbr 3938  ◡ccnv 4547  ⟶wf 5128  –1-1-onto→wf1o 5131  ‘cfv 5132   Isom wiso 5133 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4055  ax-pow 4107  ax-pr 4140 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2692  df-sbc 2915  df-un 3081  df-in 3083  df-ss 3090  df-pw 3518  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-opab 3999  df-id 4224  df-xp 4554  df-rel 4555  df-cnv 4556  df-co 4557  df-dm 4558  df-rn 4559  df-res 4560  df-ima 4561  df-iota 5097  df-fun 5134  df-fn 5135  df-f 5136  df-f1 5137  df-fo 5138  df-f1o 5139  df-fv 5140  df-isom 5141 This theorem is referenced by:  isores1  5724  isose  5731  isopo  5733  isoso  5735  isoti  6904  infrenegsupex  9436  infxrnegsupex  11084  relogiso  13022
 Copyright terms: Public domain W3C validator