This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isocnv2

Description: Converse law for isomorphism. (Contributed by Mario Carneiro, 30-Jan-2014)

		Ref	Expression
	Assertion	isocnv2	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom ^◡ 𝑅 , ^◡ 𝑆 ( 𝐴 , 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ralcom	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑦 𝑅 𝑥 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑥 ) ) )
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	brcnv	⊢ ( 𝑥 ^◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
5		fvex	⊢ ( 𝐻 ‘ 𝑥 ) ∈ V
6		fvex	⊢ ( 𝐻 ‘ 𝑦 ) ∈ V
7	5 6	brcnv	⊢ ( ( 𝐻 ‘ 𝑥 ) ^◡ 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑥 ) )
8	4 7	bibi12i	⊢ ( ( 𝑥 ^◡ 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ^◡ 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝑦 𝑅 𝑥 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑥 ) ) )
9	8	2ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ^◡ 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ^◡ 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑥 ) ) )
10	1 9	bitr4i	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑦 𝑅 𝑥 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ^◡ 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ^◡ 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
11	10	anbi2i	⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑦 𝑅 𝑥 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑥 ) ) ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ^◡ 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ^◡ 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
12		df-isom	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑦 𝑅 𝑥 ↔ ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑥 ) ) ) )
13		df-isom	⊢ ( 𝐻 Isom ^◡ 𝑅 , ^◡ 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ^◡ 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) ^◡ 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
14	11 12 13	3bitr4i	⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ 𝐻 Isom ^◡ 𝑅 , ^◡ 𝑆 ( 𝐴 , 𝐵 ) )