Theorem f1we

Description: Pull back a well ordering by a one-to-one function. (Contributed by Eric Schmidt, 4-Aug-2026)

	Ref	Expression
Hypothesis	f1owe.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) }
Assertion	f1we	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝑆 We 𝐵 → 𝑅 We 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		f1owe.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) }
2		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
3		frn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran 𝐹 ⊆ 𝐵 )
4		wess	⊢ ( ran 𝐹 ⊆ 𝐵 → ( 𝑆 We 𝐵 → 𝑆 We ran 𝐹 ) )
5	2 3 4	3syl	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝑆 We 𝐵 → 𝑆 We ran 𝐹 ) )
6		f1f1orn	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
7	1	f1owe	⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 → ( 𝑅 We 𝐴 ↔ 𝑆 We ran 𝐹 ) )
8	6 7	syl	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝑅 We 𝐴 ↔ 𝑆 We ran 𝐹 ) )
9	5 8	sylibrd	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝑆 We 𝐵 → 𝑅 We 𝐴 ) )