Metamath Proof Explorer

Theorem isocnv2

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

Ref Expression
Assertion isocnv2 ⊢HIsomR,SAB↔HIsomR-1,S-1AB

Proof

Step Hyp Ref Expression
1 ralcom ⊢∀y∈A∀x∈AyRx↔H⁡ySH⁡x↔∀x∈A∀y∈AyRx↔H⁡ySH⁡x
2 vex ⊢x∈V
3 vex ⊢y∈V
4 2 3 brcnv ⊢xR-1y↔yRx
5 fvex ⊢H⁡x∈V
6 fvex ⊢H⁡y∈V
7 5 6 brcnv ⊢H⁡xS-1H⁡y↔H⁡ySH⁡x
8 4 7 bibi12i ⊢xR-1y↔H⁡xS-1H⁡y↔yRx↔H⁡ySH⁡x
9 8 2ralbii ⊢∀x∈A∀y∈AxR-1y↔H⁡xS-1H⁡y↔∀x∈A∀y∈AyRx↔H⁡ySH⁡x
10 1 9 bitr4i ⊢∀y∈A∀x∈AyRx↔H⁡ySH⁡x↔∀x∈A∀y∈AxR-1y↔H⁡xS-1H⁡y
11 10 anbi2i ⊢H:A⟶1-1 ontoB∧∀y∈A∀x∈AyRx↔H⁡ySH⁡x↔H:A⟶1-1 ontoB∧∀x∈A∀y∈AxR-1y↔H⁡xS-1H⁡y
12 df-isom ⊢HIsomR,SAB↔H:A⟶1-1 ontoB∧∀y∈A∀x∈AyRx↔H⁡ySH⁡x
13 df-isom ⊢HIsomR-1,S-1AB↔H:A⟶1-1 ontoB∧∀x∈A∀y∈AxR-1y↔H⁡xS-1H⁡y
14 11 12 13 3bitr4i ⊢HIsomR,SAB↔HIsomR-1,S-1AB