Theorem isocnv 7278

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.

Step	Hyp	Ref	Expression
1		f1ocnv 6786	. . . 4 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → ◡𝐻:𝐵–1-1-onto→𝐴)
2	1	adantr 480	. . 3 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ◡𝐻:𝐵–1-1-onto→𝐴)
3		f1ocnvfv2 7225	. . . . . . . 8 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐻‘(◡𝐻‘𝑧)) = 𝑧)
4	3	adantrr 718	. . . . . . 7 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝐻‘(◡𝐻‘𝑧)) = 𝑧)
5		f1ocnvfv2 7225	. . . . . . . 8 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑤 ∈ 𝐵) → (𝐻‘(◡𝐻‘𝑤)) = 𝑤)
6	5	adantrl 717	. . . . . . 7 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝐻‘(◡𝐻‘𝑤)) = 𝑤)
7	4, 6	breq12d 5099	. . . . . 6 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ 𝑧𝑆𝑤))
8	7	adantlr 716	. . . . 5 ⊢ (((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ 𝑧𝑆𝑤))
9		f1of 6774	. . . . . . 7 ⊢ (◡𝐻:𝐵–1-1-onto→𝐴 → ◡𝐻:𝐵⟶𝐴)
10	1, 9	syl 17	. . . . . 6 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → ◡𝐻:𝐵⟶𝐴)
11		ffvelcdm 7027	. . . . . . . . 9 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → (◡𝐻‘𝑧) ∈ 𝐴)
12		ffvelcdm 7027	. . . . . . . . 9 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) → (◡𝐻‘𝑤) ∈ 𝐴)
13	11, 12	anim12dan 620	. . . . . . . 8 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((◡𝐻‘𝑧) ∈ 𝐴 ∧ (◡𝐻‘𝑤) ∈ 𝐴))
14		breq1 5089	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝐻‘𝑧) → (𝑥𝑅𝑦 ↔ (◡𝐻‘𝑧)𝑅𝑦))
15		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝐻‘𝑧) → (𝐻‘𝑥) = (𝐻‘(◡𝐻‘𝑧)))
16	15	breq1d 5096	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦)))
17	14, 16	bibi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ((◡𝐻‘𝑧)𝑅𝑦 ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦))))
18		bicom 222	. . . . . . . . . 10 ⊢ (((◡𝐻‘𝑧)𝑅𝑦 ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦)) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦))
19	17, 18	bitrdi 287	. . . . . . . . 9 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦)))
20		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑦 = (◡𝐻‘𝑤) → (𝐻‘𝑦) = (𝐻‘(◡𝐻‘𝑤)))
21	20	breq2d 5098	. . . . . . . . . 10 ⊢ (𝑦 = (◡𝐻‘𝑤) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤))))
22		breq2 5090	. . . . . . . . . 10 ⊢ (𝑦 = (◡𝐻‘𝑤) → ((◡𝐻‘𝑧)𝑅𝑦 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
23	21, 22	bibi12d 345	. . . . . . . . 9 ⊢ (𝑦 = (◡𝐻‘𝑤) → (((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
24	19, 23	rspc2va 3577	. . . . . . . 8 ⊢ ((((◡𝐻‘𝑧) ∈ 𝐴 ∧ (◡𝐻‘𝑤) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
25	13, 24	sylan 581	. . . . . . 7 ⊢ (((◡𝐻:𝐵⟶𝐴 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
26	25	an32s 653	. . . . . 6 ⊢ (((◡𝐻:𝐵⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
27	10, 26	sylanl1 681	. . . . 5 ⊢ (((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
28	8, 27	bitr3d 281	. . . 4 ⊢ (((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
29	28	ralrimivva 3181	. . 3 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
30	2, 29	jca 511	. 2 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (◡𝐻:𝐵–1-1-onto→𝐴 ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
31		df-isom 6501	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
32		df-isom 6501	. 2 ⊢ (◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴) ↔ (◡𝐻:𝐵–1-1-onto→𝐴 ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
33	30, 31, 32	3imtr4i 292	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052   class class class wbr 5086  ^◡ccnv 5623  ⟶wf 6488  –1-1-onto→wf1o 6491  ‘cfv 6492   Isom wiso 6493

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501

This theorem is referenced by:  isores1  7282  isofr  7290  isose  7291  isopo  7294  isoso  7296  weisoeq  7303  weisoeq2  7304  fnwelem  8074  oieu  9447  oemapwe  9606  cantnffval2  9607  wemapwe  9609  infxpenlem  9926  fpwwe2lem6  10550  fpwwe2lem8  10552  infrenegsup  12130  ltweuz  13914  fz1isolem  14414  ordthmeo  23777  relogiso  26575  erdsze2lem2  35402  fzisoeu  45751