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

Metamath Proof Explorer

Theorem f1owe

Description: Well-ordering of isomorphic relations. (Contributed by NM, 4-Mar-1997)

Ref Expression
Hypothesis f1owe.1 ⊢ R = x y | F ⁡ x S F ⁡ y
Assertion f1owe ⊢ F : A ⟶ 1-1 onto B → S We B → R We A

Proof

Step Hyp Ref Expression
1 f1owe.1 ⊢ R = x y | F ⁡ x S F ⁡ y
2 fveq2 ⊢ x = z → F ⁡ x = F ⁡ z
3 2 breq1d ⊢ x = z → F ⁡ x S F ⁡ y ↔ F ⁡ z S F ⁡ y
4 fveq2 ⊢ y = w → F ⁡ y = F ⁡ w
5 4 breq2d ⊢ y = w → F ⁡ z S F ⁡ y ↔ F ⁡ z S F ⁡ w
6 3 5 1 brabg ⊢ z ∈ A ∧ w ∈ A → z R w ↔ F ⁡ z S F ⁡ w
7 6 rgen2 ⊢ ∀ z ∈ A ∀ w ∈ A z R w ↔ F ⁡ z S F ⁡ w
8 df-isom ⊢ F Isom R , S A B ↔ F : A ⟶ 1-1 onto B ∧ ∀ z ∈ A ∀ w ∈ A z R w ↔ F ⁡ z S F ⁡ w
9 isowe ⊢ F Isom R , S A B → R We A ↔ S We B
10 8 9 sylbir ⊢ F : A ⟶ 1-1 onto B ∧ ∀ z ∈ A ∀ w ∈ A z R w ↔ F ⁡ z S F ⁡ w → R We A ↔ S We B
11 7 10 mpan2 ⊢ F : A ⟶ 1-1 onto B → R We A ↔ S We B
12 11 biimprd ⊢ F : A ⟶ 1-1 onto B → S We B → R We A