Theorem isocnv 7351

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 6859	. . . 4 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → ◡𝐻:𝐵–1-1-onto→𝐴)
2	1	adantr 480	. . 3 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ◡𝐻:𝐵–1-1-onto→𝐴)
3		f1ocnvfv2 7298	. . . . . . . 8 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑧 ∈ 𝐵) → (𝐻‘(◡𝐻‘𝑧)) = 𝑧)
4	3	adantrr 717	. . . . . . 7 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝐻‘(◡𝐻‘𝑧)) = 𝑧)
5		f1ocnvfv2 7298	. . . . . . . 8 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ 𝑤 ∈ 𝐵) → (𝐻‘(◡𝐻‘𝑤)) = 𝑤)
6	5	adantrl 716	. . . . . . 7 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝐻‘(◡𝐻‘𝑤)) = 𝑤)
7	4, 6	breq12d 5155	. . . . . 6 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ 𝑧𝑆𝑤))
8	7	adantlr 715	. . . . 5 ⊢ (((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ 𝑧𝑆𝑤))
9		f1of 6847	. . . . . . 7 ⊢ (◡𝐻:𝐵–1-1-onto→𝐴 → ◡𝐻:𝐵⟶𝐴)
10	1, 9	syl 17	. . . . . 6 ⊢ (𝐻:𝐴–1-1-onto→𝐵 → ◡𝐻:𝐵⟶𝐴)
11		ffvelcdm 7100	. . . . . . . . 9 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ 𝑧 ∈ 𝐵) → (◡𝐻‘𝑧) ∈ 𝐴)
12		ffvelcdm 7100	. . . . . . . . 9 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) → (◡𝐻‘𝑤) ∈ 𝐴)
13	11, 12	anim12dan 619	. . . . . . . 8 ⊢ ((◡𝐻:𝐵⟶𝐴 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((◡𝐻‘𝑧) ∈ 𝐴 ∧ (◡𝐻‘𝑤) ∈ 𝐴))
14		breq1 5145	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝐻‘𝑧) → (𝑥𝑅𝑦 ↔ (◡𝐻‘𝑧)𝑅𝑦))
15		fveq2 6905	. . . . . . . . . . . 12 ⊢ (𝑥 = (◡𝐻‘𝑧) → (𝐻‘𝑥) = (𝐻‘(◡𝐻‘𝑧)))
16	15	breq1d 5152	. . . . . . . . . . 11 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦)))
17	14, 16	bibi12d 345	. . . . . . . . . 10 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ((◡𝐻‘𝑧)𝑅𝑦 ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦))))
18		bicom 222	. . . . . . . . . 10 ⊢ (((◡𝐻‘𝑧)𝑅𝑦 ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦)) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦))
19	17, 18	bitrdi 287	. . . . . . . . 9 ⊢ (𝑥 = (◡𝐻‘𝑧) → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦)))
20		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑦 = (◡𝐻‘𝑤) → (𝐻‘𝑦) = (𝐻‘(◡𝐻‘𝑤)))
21	20	breq2d 5154	. . . . . . . . . 10 ⊢ (𝑦 = (◡𝐻‘𝑤) → ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤))))
22		breq2 5146	. . . . . . . . . 10 ⊢ (𝑦 = (◡𝐻‘𝑤) → ((◡𝐻‘𝑧)𝑅𝑦 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
23	21, 22	bibi12d 345	. . . . . . . . 9 ⊢ (𝑦 = (◡𝐻‘𝑤) → (((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘𝑦) ↔ (◡𝐻‘𝑧)𝑅𝑦) ↔ ((𝐻‘(◡𝐻‘𝑧))𝑆(𝐻‘(◡𝐻‘𝑤)) ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
24	19, 23	rspc2va 3633	. . . . . . . 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 3201	. . 3 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤)))
30	2, 29	jca 511	. 2 ⊢ ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (◡𝐻:𝐵–1-1-onto→𝐴 ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
31		df-isom 6569	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
32		df-isom 6569	. 2 ⊢ (◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴) ↔ (◡𝐻:𝐵–1-1-onto→𝐴 ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧𝑆𝑤 ↔ (◡𝐻‘𝑧)𝑅(◡𝐻‘𝑤))))
33	30, 31, 32	3imtr4i 292	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ◡𝐻 Isom 𝑆, 𝑅 (𝐵, 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3060   class class class wbr 5142  ^◡ccnv 5683  ⟶wf 6556  –1-1-onto→wf1o 6559  ‘cfv 6560   Isom wiso 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569

This theorem is referenced by:  isores1  7355  isofr  7363  isose  7364  isopo  7367  isoso  7369  weisoeq  7376  weisoeq2  7377  fnwelem  8157  oieu  9580  oemapwe  9735  cantnffval2  9736  wemapwe  9738  infxpenlem  10054  fpwwe2lem6  10677  fpwwe2lem8  10679  infrenegsup  12252  ltweuz  14003  fz1isolem  14501  ordthmeo  23811  relogiso  26641  erdsze2lem2  35210  fzisoeu  45317