Metamath Proof Explorer

Theorem isores1

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 isores1 ⊢ H Isom R , S A B ↔ H Isom R ∩ A × A , S A B

Proof

Step Hyp Ref Expression
1 isocnv ⊢ H Isom R , S A B → H -1 Isom S , R B A
2 isores2 ⊢ H -1 Isom S , R B A ↔ H -1 Isom S , R ∩ A × A B A
3 1 2 sylib ⊢ H Isom R , S A B → H -1 Isom S , R ∩ A × A B A
4 isocnv ⊢ H -1 Isom S , R ∩ A × A B A → H -1 -1 Isom R ∩ A × A , S A B
5 3 4 syl ⊢ H Isom R , S A B → H -1 -1 Isom R ∩ A × A , S A B
6 isof1o ⊢ H Isom R , S A B → H : A ⟶ 1-1 onto B
7 f1orel ⊢ H : A ⟶ 1-1 onto B → Rel ⁡ H
8 dfrel2 ⊢ Rel ⁡ H ↔ H -1 -1 = H
9 isoeq1 ⊢ H -1 -1 = H → H -1 -1 Isom R ∩ A × A , S A B ↔ H Isom R ∩ A × A , S A B
10 8 9 sylbi ⊢ Rel ⁡ H → H -1 -1 Isom R ∩ A × A , S A B ↔ H Isom R ∩ A × A , S A B
11 6 7 10 3syl ⊢ H Isom R , S A B → H -1 -1 Isom R ∩ A × A , S A B ↔ H Isom R ∩ A × A , S A B
12 5 11 mpbid ⊢ H Isom R , S A B → H Isom R ∩ A × A , S A B
13 isocnv ⊢ H Isom R ∩ A × A , S A B → H -1 Isom S , R ∩ A × A B A
14 13 2 sylibr ⊢ H Isom R ∩ A × A , S A B → H -1 Isom S , R B A
15 isocnv ⊢ H -1 Isom S , R B A → H -1 -1 Isom R , S A B
16 14 15 syl ⊢ H Isom R ∩ A × A , S A B → H -1 -1 Isom R , S A B
17 isof1o ⊢ H Isom R ∩ A × A , S A B → H : A ⟶ 1-1 onto B
18 isoeq1 ⊢ H -1 -1 = H → H -1 -1 Isom R , S A B ↔ H Isom R , S A B
19 8 18 sylbi ⊢ Rel ⁡ H → H -1 -1 Isom R , S A B ↔ H Isom R , S A B
20 17 7 19 3syl ⊢ H Isom R ∩ A × A , S A B → H -1 -1 Isom R , S A B ↔ H Isom R , S A B
21 16 20 mpbid ⊢ H Isom R ∩ A × A , S A B → H Isom R , S A B
22 12 21 impbii ⊢ H Isom R , S A B ↔ H Isom R ∩ A × A , S A B