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 ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )

Proof

Step Hyp Ref Expression
1 f1ocnv ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐻 : 𝐵 –1-1-onto→ 𝐴 )
2 1 adantr ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → ◡ 𝐻 : 𝐵 –1-1-onto→ 𝐴 )
3 f1ocnvfv2 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) = 𝑧 )
4 3 adantrr ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) = 𝑧 )
5 f1ocnvfv2 ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) = 𝑤 )
6 5 adantrl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) = 𝑤 )
7 4 6 breq12d ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) ↔ 𝑧 𝑆 𝑤 ) )
8 7 adantlr ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) ↔ 𝑧 𝑆 𝑤 ) )
9 f1of ⊢ ( ◡ 𝐻 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐻 : 𝐵 ⟶ 𝐴 )
10 1 9 syl ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐻 : 𝐵 ⟶ 𝐴 )
11 ffvelrn ⊢ ( ( ◡ 𝐻 : 𝐵 ⟶ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( ◡ 𝐻 ‘ 𝑧 ) ∈ 𝐴 )
12 ffvelrn ⊢ ( ( ◡ 𝐻 : 𝐵 ⟶ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( ◡ 𝐻 ‘ 𝑤 ) ∈ 𝐴 )
13 11 12 anim12dan ⊢ ( ( ◡ 𝐻 : 𝐵 ⟶ 𝐴 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ◡ 𝐻 ‘ 𝑧 ) ∈ 𝐴 ∧ ( ◡ 𝐻 ‘ 𝑤 ) ∈ 𝐴 ) )
14 breq1 ⊢ ( 𝑥 = ( ◡ 𝐻 ‘ 𝑧 ) → ( 𝑥 𝑅 𝑦 ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 𝑦 ) )
15 fveq2 ⊢ ( 𝑥 = ( ◡ 𝐻 ‘ 𝑧 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) )
16 15 breq1d ⊢ ( 𝑥 = ( ◡ 𝐻 ‘ 𝑧 ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
17 14 16 bibi12d ⊢ ( 𝑥 = ( ◡ 𝐻 ‘ 𝑧 ) → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 𝑦 ↔ ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
18 bicom ⊢ ( ( ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 𝑦 ↔ ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 𝑦 ) )
19 17 18 bitrdi ⊢ ( 𝑥 = ( ◡ 𝐻 ‘ 𝑧 ) → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 𝑦 ) ) )
20 fveq2 ⊢ ( 𝑦 = ( ◡ 𝐻 ‘ 𝑤 ) → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) )
21 20 breq2d ⊢ ( 𝑦 = ( ◡ 𝐻 ‘ 𝑤 ) → ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) ) )
22 breq2 ⊢ ( 𝑦 = ( ◡ 𝐻 ‘ 𝑤 ) → ( ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 𝑦 ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) )
23 21 22 bibi12d ⊢ ( 𝑦 = ( ◡ 𝐻 ‘ 𝑤 ) → ( ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 𝑦 ) ↔ ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) ) )
24 19 23 rspc2va ⊢ ( ( ( ( ◡ 𝐻 ‘ 𝑧 ) ∈ 𝐴 ∧ ( ◡ 𝐻 ‘ 𝑤 ) ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) )
25 13 24 sylan ⊢ ( ( ( ◡ 𝐻 : 𝐵 ⟶ 𝐴 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) )
26 25 an32s ⊢ ( ( ( ◡ 𝐻 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) )
27 10 26 sylanl1 ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑧 ) ) 𝑆 ( 𝐻 ‘ ( ◡ 𝐻 ‘ 𝑤 ) ) ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) )
28 8 27 bitr3d ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 𝑆 𝑤 ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) )
29 28 ralrimivva ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) )
30 2 29 jca ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → ( ◡ 𝐻 : 𝐵 –1-1-onto→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) ) )
31 df-isom ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
32 df-isom ⊢ ( ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) ↔ ( ◡ 𝐻 : 𝐵 –1-1-onto→ 𝐴 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( ◡ 𝐻 ‘ 𝑧 ) 𝑅 ( ◡ 𝐻 ‘ 𝑤 ) ) ) )
33 30 31 32 3imtr4i ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ◡ 𝐻 Isom 𝑆 , 𝑅 ( 𝐵 , 𝐴 ) )