Theorem prconf1acwevd

Description: If F maps the proper class W one-to-one into the ordinals and the Axiom of Choice holds, then R well-orders the universe. (Contributed by BTernaryTau, 16-Sep-2026)

	Ref	Expression
Hypotheses	prconf1acwevd.1	⊢ ( 𝜑 → ( ¬ 𝑊 ∈ V → 𝐹 : 𝑊 –1-1→ On ) )
	prconf1acwevd.2	⊢ ( 𝜑 → CHOICE )
	prconf1acwevd.3	⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
	prconf1acwevd.4	⊢ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝑆 𝑧 ) ) }
	prconf1acwevd.5	⊢ 𝑆 = ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
Assertion	prconf1acwevd	⊢ ( 𝜑 → 𝑅 We V )

Proof

Step	Hyp	Ref	Expression
1		prconf1acwevd.1	⊢ ( 𝜑 → ( ¬ 𝑊 ∈ V → 𝐹 : 𝑊 –1-1→ On ) )
2		prconf1acwevd.2	⊢ ( 𝜑 → CHOICE )
3		prconf1acwevd.3	⊢ 𝑊 = { 𝑟 ∣ ∃ 𝑥 ∈ On ( 𝑟 ⊆ ( ( 𝑅1 ‘ 𝑥 ) × ( 𝑅1 ‘ 𝑥 ) ) ∧ 𝑟 We ( 𝑅1 ‘ 𝑥 ) ) }
4		prconf1acwevd.4	⊢ 𝑅 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑧 ) ∨ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑧 ) ∧ 𝑦 𝑆 𝑧 ) ) }
5		prconf1acwevd.5	⊢ 𝑆 = ( ◡ 𝐹 ‘ ∩ { 𝑤 ∈ On ∣ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) } )
6	3	acwer1prc	⊢ ( CHOICE → ¬ 𝑊 ∈ V )
7	2 6	syl	⊢ ( 𝜑 → ¬ 𝑊 ∈ V )
8	7 1	mpd	⊢ ( 𝜑 → 𝐹 : 𝑊 –1-1→ On )
9		f1f	⊢ ( 𝐹 : 𝑊 –1-1→ On → 𝐹 : 𝑊 ⟶ On )
10		frn	⊢ ( 𝐹 : 𝑊 ⟶ On → ran 𝐹 ⊆ On )
11	8 9 10	3syl	⊢ ( 𝜑 → ran 𝐹 ⊆ On )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ran 𝐹 ⊆ On )
13		ssid	⊢ 𝑊 ⊆ 𝑊
14	3	onprcf1acwevdlem1	⊢ ( ( 𝑊 ⊆ 𝑊 ∧ 𝑣 ∈ On ∧ ∀ 𝑢 ∈ 𝑊 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) ) → 𝑊 ∈ V )
15	13 14	mp3an1	⊢ ( ( 𝑣 ∈ On ∧ ∀ 𝑢 ∈ 𝑊 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) ) → 𝑊 ∈ V )
16	15	ex	⊢ ( 𝑣 ∈ On → ( ∀ 𝑢 ∈ 𝑊 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) → 𝑊 ∈ V ) )
17	16 7	nsyli	⊢ ( 𝑣 ∈ On → ( 𝜑 → ¬ ∀ 𝑢 ∈ 𝑊 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) ) )
18	17	impcom	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ¬ ∀ 𝑢 ∈ 𝑊 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) )
19		dfrex2	⊢ ( ∃ 𝑢 ∈ 𝑊 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ¬ ∀ 𝑢 ∈ 𝑊 ¬ 𝑢 We ( 𝑅1 ‘ 𝑣 ) )
20	18 19	sylibr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ∃ 𝑢 ∈ 𝑊 𝑢 We ( 𝑅1 ‘ 𝑣 ) )
21		f1f1orn	⊢ ( 𝐹 : 𝑊 –1-1→ On → 𝐹 : 𝑊 –1-1-onto→ ran 𝐹 )
22		f1ocnv	⊢ ( 𝐹 : 𝑊 –1-1-onto→ ran 𝐹 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝑊 )
23	8 21 22	3syl	⊢ ( 𝜑 → ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝑊 )
24		f1ofo	⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝑊 → ◡ 𝐹 : ran 𝐹 –onto→ 𝑊 )
25		forn	⊢ ( ◡ 𝐹 : ran 𝐹 –onto→ 𝑊 → ran ◡ 𝐹 = 𝑊 )
26	23 24 25	3syl	⊢ ( 𝜑 → ran ◡ 𝐹 = 𝑊 )
27	26	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ran ◡ 𝐹 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ∃ 𝑢 ∈ 𝑊 𝑢 We ( 𝑅1 ‘ 𝑣 ) ) )
28		f1ofn	⊢ ( ◡ 𝐹 : ran 𝐹 –1-1-onto→ 𝑊 → ◡ 𝐹 Fn ran 𝐹 )
29		weeq1	⊢ ( 𝑢 = ( ◡ 𝐹 ‘ 𝑤 ) → ( 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
30	29	rexrn	⊢ ( ◡ 𝐹 Fn ran 𝐹 → ( ∃ 𝑢 ∈ ran ◡ 𝐹 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ∃ 𝑤 ∈ ran 𝐹 ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
31	23 28 30	3syl	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ran ◡ 𝐹 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ∃ 𝑤 ∈ ran 𝐹 ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
32	27 31	bitr3d	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ 𝑊 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ∃ 𝑤 ∈ ran 𝐹 ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ( ∃ 𝑢 ∈ 𝑊 𝑢 We ( 𝑅1 ‘ 𝑣 ) ↔ ∃ 𝑤 ∈ ran 𝐹 ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
34	20 33	mpbid	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ∃ 𝑤 ∈ ran 𝐹 ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) )
35		ssrexv	⊢ ( ran 𝐹 ⊆ On → ( ∃ 𝑤 ∈ ran 𝐹 ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) → ∃ 𝑤 ∈ On ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) ) )
36	12 34 35	sylc	⊢ ( ( 𝜑 ∧ 𝑣 ∈ On ) → ∃ 𝑤 ∈ On ( ◡ 𝐹 ‘ 𝑤 ) We ( 𝑅1 ‘ 𝑣 ) )
37	4 5 36	onprcf1acwevdlem2	⊢ ( 𝜑 → 𝑅 We V )