Metamath Proof Explorer

Theorem isores2

Description: An isomorphism from one well-order to another can be restricted on either well-order. (Contributed by Mario Carneiro, 15-Jan-2013)

Ref Expression
Assertion isores2 ⊢ H Isom R , S A B ↔ H Isom R , S ∩ B × B A B

Proof

Step Hyp Ref Expression
1 f1of ⊢ H : A ⟶ 1-1 onto B → H : A ⟶ B
2 ffvelrn ⊢ H : A ⟶ B ∧ x ∈ A → H ⁡ x ∈ B
3 2 adantrr ⊢ H : A ⟶ B ∧ x ∈ A ∧ y ∈ A → H ⁡ x ∈ B
4 ffvelrn ⊢ H : A ⟶ B ∧ y ∈ A → H ⁡ y ∈ B
5 4 adantrl ⊢ H : A ⟶ B ∧ x ∈ A ∧ y ∈ A → H ⁡ y ∈ B
6 brinxp ⊢ H ⁡ x ∈ B ∧ H ⁡ y ∈ B → H ⁡ x S H ⁡ y ↔ H ⁡ x S ∩ B × B H ⁡ y
7 3 5 6 syl2anc ⊢ H : A ⟶ B ∧ x ∈ A ∧ y ∈ A → H ⁡ x S H ⁡ y ↔ H ⁡ x S ∩ B × B H ⁡ y
8 1 7 sylan ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A ∧ y ∈ A → H ⁡ x S H ⁡ y ↔ H ⁡ x S ∩ B × B H ⁡ y
9 8 anassrs ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A ∧ y ∈ A → H ⁡ x S H ⁡ y ↔ H ⁡ x S ∩ B × B H ⁡ y
10 9 bibi2d ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A ∧ y ∈ A → x R y ↔ H ⁡ x S H ⁡ y ↔ x R y ↔ H ⁡ x S ∩ B × B H ⁡ y
11 10 ralbidva ⊢ H : A ⟶ 1-1 onto B ∧ x ∈ A → ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ ∀ y ∈ A x R y ↔ H ⁡ x S ∩ B × B H ⁡ y
12 11 ralbidva ⊢ H : A ⟶ 1-1 onto B → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S ∩ B × B H ⁡ y
13 12 pm5.32i ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S ∩ B × B H ⁡ y
14 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
15 df-isom ⊢ H Isom R , S ∩ B × B A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S ∩ B × B H ⁡ y
16 13 14 15 3bitr4i ⊢ H Isom R , S A B ↔ H Isom R , S ∩ B × B A B