Metamath Proof Explorer

Theorem isocnv

Description: Converse law for isomorphism. Proposition 6.30(2) of TakeutiZaring p. 33. (Contributed by NM, 27-Apr-2004)

Ref Expression
Assertion isocnv ⊢ H Isom R , S A B → H -1 Isom S , R B A

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ H : A ⟶ 1-1 onto B → H -1 : B ⟶ 1-1 onto A
2 1 adantr ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y → H -1 : B ⟶ 1-1 onto A
3 f1ocnvfv2 ⊢ H : A ⟶ 1-1 onto B ∧ z ∈ B → H ⁡ H -1 ⁡ z = z
4 3 adantrr ⊢ H : A ⟶ 1-1 onto B ∧ z ∈ B ∧ w ∈ B → H ⁡ H -1 ⁡ z = z
5 f1ocnvfv2 ⊢ H : A ⟶ 1-1 onto B ∧ w ∈ B → H ⁡ H -1 ⁡ w = w
6 5 adantrl ⊢ H : A ⟶ 1-1 onto B ∧ z ∈ B ∧ w ∈ B → H ⁡ H -1 ⁡ w = w
7 4 6 breq12d ⊢ H : A ⟶ 1-1 onto B ∧ z ∈ B ∧ w ∈ B → H ⁡ H -1 ⁡ z S H ⁡ H -1 ⁡ w ↔ z S w
8 7 adantlr ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ∧ z ∈ B ∧ w ∈ B → H ⁡ H -1 ⁡ z S H ⁡ H -1 ⁡ w ↔ z S w
9 f1of ⊢ H -1 : B ⟶ 1-1 onto A → H -1 : B ⟶ A
10 1 9 syl ⊢ H : A ⟶ 1-1 onto B → H -1 : B ⟶ A
11 ffvelrn ⊢ H -1 : B ⟶ A ∧ z ∈ B → H -1 ⁡ z ∈ A
12 ffvelrn ⊢ H -1 : B ⟶ A ∧ w ∈ B → H -1 ⁡ w ∈ A
13 11 12 anim12dan ⊢ H -1 : B ⟶ A ∧ z ∈ B ∧ w ∈ B → H -1 ⁡ z ∈ A ∧ H -1 ⁡ w ∈ A
14 breq1 ⊢ x = H -1 ⁡ z → x R y ↔ H -1 ⁡ z R y
15 fveq2 ⊢ x = H -1 ⁡ z → H ⁡ x = H ⁡ H -1 ⁡ z
16 15 breq1d ⊢ x = H -1 ⁡ z → H ⁡ x S H ⁡ y ↔ H ⁡ H -1 ⁡ z S H ⁡ y
17 14 16 bibi12d ⊢ x = H -1 ⁡ z → x R y ↔ H ⁡ x S H ⁡ y ↔ H -1 ⁡ z R y ↔ H ⁡ H -1 ⁡ z S H ⁡ y
18 bicom ⊢ H -1 ⁡ z R y ↔ H ⁡ H -1 ⁡ z S H ⁡ y ↔ H ⁡ H -1 ⁡ z S H ⁡ y ↔ H -1 ⁡ z R y
19 17 18 bitrdi ⊢ x = H -1 ⁡ z → x R y ↔ H ⁡ x S H ⁡ y ↔ H ⁡ H -1 ⁡ z S H ⁡ y ↔ H -1 ⁡ z R y
20 fveq2 ⊢ y = H -1 ⁡ w → H ⁡ y = H ⁡ H -1 ⁡ w
21 20 breq2d ⊢ y = H -1 ⁡ w → H ⁡ H -1 ⁡ z S H ⁡ y ↔ H ⁡ H -1 ⁡ z S H ⁡ H -1 ⁡ w
22 breq2 ⊢ y = H -1 ⁡ w → H -1 ⁡ z R y ↔ H -1 ⁡ z R H -1 ⁡ w
23 21 22 bibi12d ⊢ y = H -1 ⁡ w → H ⁡ H -1 ⁡ z S H ⁡ y ↔ H -1 ⁡ z R y ↔ H ⁡ H -1 ⁡ z S H ⁡ H -1 ⁡ w ↔ H -1 ⁡ z R H -1 ⁡ w
24 19 23 rspc2va ⊢ H -1 ⁡ z ∈ A ∧ H -1 ⁡ w ∈ A ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y → H ⁡ H -1 ⁡ z S H ⁡ H -1 ⁡ w ↔ H -1 ⁡ z R H -1 ⁡ w
25 13 24 sylan ⊢ H -1 : B ⟶ A ∧ z ∈ B ∧ w ∈ B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y → H ⁡ H -1 ⁡ z S H ⁡ H -1 ⁡ w ↔ H -1 ⁡ z R H -1 ⁡ w
26 25 an32s ⊢ H -1 : B ⟶ A ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ∧ z ∈ B ∧ w ∈ B → H ⁡ H -1 ⁡ z S H ⁡ H -1 ⁡ w ↔ H -1 ⁡ z R H -1 ⁡ w
27 10 26 sylanl1 ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ∧ z ∈ B ∧ w ∈ B → H ⁡ H -1 ⁡ z S H ⁡ H -1 ⁡ w ↔ H -1 ⁡ z R H -1 ⁡ w
28 8 27 bitr3d ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ∧ z ∈ B ∧ w ∈ B → z S w ↔ H -1 ⁡ z R H -1 ⁡ w
29 28 ralrimivva ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y → ∀ z ∈ B ∀ w ∈ B z S w ↔ H -1 ⁡ z R H -1 ⁡ w
30 2 29 jca ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y → H -1 : B ⟶ 1-1 onto A ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ H -1 ⁡ z R H -1 ⁡ w
31 df-isom ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
32 df-isom ⊢ H -1 Isom S , R B A ↔ H -1 : B ⟶ 1-1 onto A ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ H -1 ⁡ z R H -1 ⁡ w
33 30 31 32 3imtr4i ⊢ H Isom R , S A B → H -1 Isom S , R B A