Theorem onf1we

Description: If F maps A one-to-one into the ordinals, then R well-orders A . (Contributed by BTernaryTau, 16-Sep-2026)

	Ref	Expression
Hypothesis	onf1we.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
Assertion	onf1we	⊢ ( 𝐹 : 𝐴 –1-1→ On → 𝑅 We 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		onf1we.1	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
2		f1f	⊢ ( 𝐹 : 𝐴 –1-1→ On → 𝐹 : 𝐴 ⟶ On )
3	2	frnd	⊢ ( 𝐹 : 𝐴 –1-1→ On → ran 𝐹 ⊆ On )
4		epweon	⊢ E We On
5		wess	⊢ ( ran 𝐹 ⊆ On → ( E We On → E We ran 𝐹 ) )
6	3 4 5	mpisyl	⊢ ( 𝐹 : 𝐴 –1-1→ On → E We ran 𝐹 )
7		f1f1orn	⊢ ( 𝐹 : 𝐴 –1-1→ On → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 )
8		fvex	⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
9	8	epeli	⊢ ( ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) )
10	9	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
11	1 10	eqtr4i	⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) }
12	11	f1owe	⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 → ( 𝑅 We 𝐴 ↔ E We ran 𝐹 ) )
13	7 12	syl	⊢ ( 𝐹 : 𝐴 –1-1→ On → ( 𝑅 We 𝐴 ↔ E We ran 𝐹 ) )
14	6 13	mpbird	⊢ ( 𝐹 : 𝐴 –1-1→ On → 𝑅 We 𝐴 )