Theorem wevonprcf1o

Description: If R is a set-like well-ordering of the universe and A is a proper class, then F is a bijection from the ordinals to A . This is the ZFC version of (4 -> 5) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 9-Jun-2026)

	Ref	Expression
Hypothesis	wevonprcf1o.1	|- F = OrdIso ( R , A )
Assertion	wevonprcf1o	|- ( ( R We _V /\ R Se _V /\ -. A e. _V ) -> F : On -1-1-onto-> A )

Proof

Step	Hyp	Ref	Expression
1		wevonprcf1o.1	|- F = OrdIso ( R , A )
2		ssv	|- A C_ _V
3		wess	|- ( A C_ _V -> ( R We _V -> R We A ) )
4	2 3	ax-mp	|- ( R We _V -> R We A )
5		sess2	|- ( A C_ _V -> ( R Se _V -> R Se A ) )
6	2 5	ax-mp	|- ( R Se _V -> R Se A )
7		id	|- ( -. A e. _V -> -. A e. _V )
8	4 6 7	3anim123i	|- ( ( R We _V /\ R Se _V /\ -. A e. _V ) -> ( R We A /\ R Se A /\ -. A e. _V ) )
9	1	ordtypeon	|- ( ( R We A /\ R Se A /\ -. A e. _V ) -> F Isom _E , R ( On , A ) )
10		isof1o	|- ( F Isom _E , R ( On , A ) -> F : On -1-1-onto-> A )
11	8 9 10	3syl	|- ( ( R We _V /\ R Se _V /\ -. A e. _V ) -> F : On -1-1-onto-> A )