Theorem isocnv 7305

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 6812	. . . 4 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → ◡𝐻:𝐵–1-1-onto→𝐴)
2	1	adantr 480	. . 3 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ◡𝐻:𝐵–1-1-onto→𝐴)
3		f1ocnvfv2 7252	. . . . . . . 8 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐻‘(◡𝐻‘𝑧)) = 𝑧)
4	3	adantrr 717	. . . . . . 7 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝐻‘(◡𝐻‘𝑧)) = 𝑧)
5		f1ocnvfv2 7252	. . . . . . . 8 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑤 ∈ 𝐵) → (𝐻‘(◡𝐻‘𝑤)) = 𝑤)
6	5	adantrl 716	. . . . . . 7 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝐻‘(◡𝐻‘𝑤)) = 𝑤)
7	4, 6	breq12d 5120	. . . . . 6 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ 𝑧𝑆𝑤))
8	7	adantlr 715	. . . . 5 ⊢ (((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ 𝑧𝑆𝑤))
9		f1of 6800	. . . . . . 7 ⊢ (◡𝐻:𝐵–1-1-onto→𝐴 → ◡𝐻:𝐵⟶𝐴)
10	1, 9	syl 17	. . . . . 6 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → ◡𝐻:𝐵⟶𝐴)
11		ffvelcdm 7053	. . . . . . . . 9 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → (◡𝐻‘𝑧) ∈ 𝐴)
12		ffvelcdm 7053	. . . . . . . . 9 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) → (◡𝐻‘𝑤) ∈ 𝐴)
13	11, 12	anim12dan 619	. . . . . . . 8 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((◡𝐻‘𝑧) ∈ 𝐴 ∧ (◡𝐻‘𝑤) ∈ 𝐴))
14		breq1 5110	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝐻‘𝑧) → (𝑥𝑅𝑦 ↔ (◡𝐻‘𝑧)𝑅𝑦))
15		fveq2 6858	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝐻‘𝑧) → (𝐻‘𝑥) = (𝐻‘(◡𝐻‘𝑧)))
16	15	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦)))
17	14, 16	bibi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ((◡𝐻‘𝑧)𝑅𝑦 ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦))))
18		bicom 222	. . . . . . . . . 10 ⊢ (((◡𝐻‘𝑧)𝑅𝑦 ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦)) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦))
19	17, 18	bitrdi 287	. . . . . . . . 9 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦)))
20		fveq2 6858	. . . . . . . . . . 11 ⊢ (𝑦 = (◡𝐻‘𝑤) → (𝐻‘𝑦) = (𝐻‘(◡𝐻‘𝑤)))
21	20	breq2d 5119	. . . . . . . . . 10 ⊢ (𝑦 = (◡𝐻‘𝑤) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤))))
22		breq2 5111	. . . . . . . . . 10 ⊢ (𝑦 = (◡𝐻‘𝑤) → ((◡𝐻‘𝑧)𝑅𝑦 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
23	21, 22	bibi12d 345	. . . . . . . . 9 ⊢ (𝑦 = (◡𝐻‘𝑤) → (((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
24	19, 23	rspc2va 3600	. . . . . . . 8 ⊢ ((((◡𝐻‘𝑧) ∈ 𝐴 ∧ (◡𝐻‘𝑤) ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
25	13, 24	sylan 580	. . . . . . 7 ⊢ (((◡𝐻:𝐵⟶𝐴 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
26	25	an32s 652	. . . . . 6 ⊢ (((◡𝐻:𝐵⟶𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
27	10, 26	sylanl1 680	. . . . 5 ⊢ (((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
28	8, 27	bitr3d 281	. . . 4 ⊢ (((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
29	28	ralrimivva 3180	. . 3 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
30	2, 29	jca 511	. 2 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (◡𝐻:𝐵–1-1-onto→𝐴 ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
31		df-isom 6520	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
32		df-isom 6520	. 2 ⊢ (◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴) ↔ (◡𝐻:𝐵–1-1-onto→𝐴 ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
33	30, 31, 32	3imtr4i 292	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044   class class class wbr 5107  ^◡ccnv 5637  ⟶wf 6507  –1-1-onto→wf1o 6510  ‘cfv 6511   Isom wiso 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520

This theorem is referenced by:  isores1  7309  isofr  7317  isose  7318  isopo  7321  isoso  7323  weisoeq  7330  weisoeq2  7331  fnwelem  8110  oieu  9492  oemapwe  9647  cantnffval2  9648  wemapwe  9650  infxpenlem  9966  fpwwe2lem6  10589  fpwwe2lem8  10591  infrenegsup  12166  ltweuz  13926  fz1isolem  14426  ordthmeo  23689  relogiso  26507  erdsze2lem2  35191  fzisoeu  45298