Metamath Proof Explorer

Theorem isocnv2

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

Ref Expression
Assertion isocnv2 ⊢ H Isom R , S A B ↔ H Isom R -1 , S -1 A B

Proof

Step Hyp Ref Expression
1 ralcom ⊢ ∀ y ∈ A ∀ x ∈ A y R x ↔ H ⁡ y S H ⁡ x ↔ ∀ x ∈ A ∀ y ∈ A y R x ↔ H ⁡ y S H ⁡ x
2 vex ⊢ x ∈ V
3 vex ⊢ y ∈ V
4 2 3 brcnv ⊢ x R -1 y ↔ y R x
5 fvex ⊢ H ⁡ x ∈ V
6 fvex ⊢ H ⁡ y ∈ V
7 5 6 brcnv ⊢ H ⁡ x S -1 H ⁡ y ↔ H ⁡ y S H ⁡ x
8 4 7 bibi12i ⊢ x R -1 y ↔ H ⁡ x S -1 H ⁡ y ↔ y R x ↔ H ⁡ y S H ⁡ x
9 8 2ralbii ⊢ ∀ x ∈ A ∀ y ∈ A x R -1 y ↔ H ⁡ x S -1 H ⁡ y ↔ ∀ x ∈ A ∀ y ∈ A y R x ↔ H ⁡ y S H ⁡ x
10 1 9 bitr4i ⊢ ∀ y ∈ A ∀ x ∈ A y R x ↔ H ⁡ y S H ⁡ x ↔ ∀ x ∈ A ∀ y ∈ A x R -1 y ↔ H ⁡ x S -1 H ⁡ y
11 10 anbi2i ⊢ H : A ⟶ 1-1 onto B ∧ ∀ y ∈ A ∀ x ∈ A y R x ↔ H ⁡ y S H ⁡ x ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R -1 y ↔ H ⁡ x S -1 H ⁡ y
12 df-isom ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ y ∈ A ∀ x ∈ A y R x ↔ H ⁡ y S H ⁡ x
13 df-isom ⊢ H Isom R -1 , S -1 A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R -1 y ↔ H ⁡ x S -1 H ⁡ y
14 11 12 13 3bitr4i ⊢ H Isom R , S A B ↔ H Isom R -1 , S -1 A B