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 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) }
Assertion f1owe ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑆 We 𝐵 → 𝑅 We 𝐴 ) )

Proof

Step Hyp Ref Expression
1 f1owe.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) }
2 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
3 2 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
4 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
5 4 breq2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
6 3 5 1 brabg ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑧 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
7 6 rgen2 ⊢ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) )
8 df-isom ⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ) )
9 isowe ⊢ ( 𝐹 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑅 We 𝐴 ↔ 𝑆 We 𝐵 ) )
10 8 9 sylbir ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ) → ( 𝑅 We 𝐴 ↔ 𝑆 We 𝐵 ) )
11 7 10 mpan2 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑅 We 𝐴 ↔ 𝑆 We 𝐵 ) )
12 11 biimprd ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑆 We 𝐵 → 𝑅 We 𝐴 ) )