Theorem wevgblacfn

Description: If R is a well-ordering of the universe, then F is a global choice function. Here F maps each set z to its minimal element with respect to R (except when z is the empty set, in which case it is mapped to the empty set, though this is only done for convenience). (Contributed by BTernaryTau, 29-Jun-2025)

	Ref	Expression
Hypothesis	wevgblacfn.1	⊢ 𝐹 = ( 𝑧 ∈ V ↦ ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } )
Assertion	wevgblacfn	⊢ ( 𝑅 We V → ( 𝐹 Fn V ∧ ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		wevgblacfn.1	⊢ 𝐹 = ( 𝑧 ∈ V ↦ ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } )
2		eleq2	⊢ ( 𝑧 = ∅ → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ∅ ) )
3		raleq	⊢ ( 𝑧 = ∅ → ( ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∈ ∅ ¬ 𝑥 𝑅 𝑦 ) )
4	2 3	anbi12d	⊢ ( 𝑧 = ∅ → ( ( 𝑦 ∈ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 ) ↔ ( 𝑦 ∈ ∅ ∧ ∀ 𝑥 ∈ ∅ ¬ 𝑥 𝑅 𝑦 ) ) )
5	4	rabbidva2	⊢ ( 𝑧 = ∅ → { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑦 ∈ ∅ ∣ ∀ 𝑥 ∈ ∅ ¬ 𝑥 𝑅 𝑦 } )
6	5	unieqd	⊢ ( 𝑧 = ∅ → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = ∪ { 𝑦 ∈ ∅ ∣ ∀ 𝑥 ∈ ∅ ¬ 𝑥 𝑅 𝑦 } )
7		rab0	⊢ { 𝑦 ∈ ∅ ∣ ∀ 𝑥 ∈ ∅ ¬ 𝑥 𝑅 𝑦 } = ∅
8	7	unieqi	⊢ ∪ { 𝑦 ∈ ∅ ∣ ∀ 𝑥 ∈ ∅ ¬ 𝑥 𝑅 𝑦 } = ∪ ∅
9		uni0	⊢ ∪ ∅ = ∅
10	8 9	eqtri	⊢ ∪ { 𝑦 ∈ ∅ ∣ ∀ 𝑥 ∈ ∅ ¬ 𝑥 𝑅 𝑦 } = ∅
11	6 10	eqtrdi	⊢ ( 𝑧 = ∅ → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = ∅ )
12		0ex	⊢ ∅ ∈ V
13	11 12	eqeltrdi	⊢ ( 𝑧 = ∅ → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ V )
14	13	adantl	⊢ ( ( 𝑅 We V ∧ 𝑧 = ∅ ) → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ V )
15		ssv	⊢ 𝑧 ⊆ V
16	15	jctl	⊢ ( 𝑧 ≠ ∅ → ( 𝑧 ⊆ V ∧ 𝑧 ≠ ∅ ) )
17		vex	⊢ 𝑧 ∈ V
18	16 17	jctil	⊢ ( 𝑧 ≠ ∅ → ( 𝑧 ∈ V ∧ ( 𝑧 ⊆ V ∧ 𝑧 ≠ ∅ ) ) )
19		3anass	⊢ ( ( 𝑧 ∈ V ∧ 𝑧 ⊆ V ∧ 𝑧 ≠ ∅ ) ↔ ( 𝑧 ∈ V ∧ ( 𝑧 ⊆ V ∧ 𝑧 ≠ ∅ ) ) )
20	18 19	sylibr	⊢ ( 𝑧 ≠ ∅ → ( 𝑧 ∈ V ∧ 𝑧 ⊆ V ∧ 𝑧 ≠ ∅ ) )
21		wereu	⊢ ( ( 𝑅 We V ∧ ( 𝑧 ∈ V ∧ 𝑧 ⊆ V ∧ 𝑧 ≠ ∅ ) ) → ∃! 𝑦 ∈ 𝑧 ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 )
22	20 21	sylan2	⊢ ( ( 𝑅 We V ∧ 𝑧 ≠ ∅ ) → ∃! 𝑦 ∈ 𝑧 ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 )
23		vsnid	⊢ 𝑤 ∈ { 𝑤 }
24		eleq2	⊢ ( { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑤 } → ( 𝑤 ∈ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ↔ 𝑤 ∈ { 𝑤 } ) )
25	23 24	mpbiri	⊢ ( { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑤 } → 𝑤 ∈ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } )
26		elrabi	⊢ ( 𝑤 ∈ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } → 𝑤 ∈ 𝑧 )
27	25 26	syl	⊢ ( { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑤 } → 𝑤 ∈ 𝑧 )
28		unieq	⊢ ( { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑤 } → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = ∪ { 𝑤 } )
29		unisnv	⊢ ∪ { 𝑤 } = 𝑤
30	28 29	eqtrdi	⊢ ( { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑤 } → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 )
31	27 30	jca	⊢ ( { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑤 } → ( 𝑤 ∈ 𝑧 ∧ ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 ) )
32	31	eximi	⊢ ( ∃ 𝑤 { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑤 } → ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 ) )
33		reusn	⊢ ( ∃! 𝑦 ∈ 𝑧 ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 ↔ ∃ 𝑤 { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = { 𝑤 } )
34		df-rex	⊢ ( ∃ 𝑤 ∈ 𝑧 ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 ) )
35	32 33 34	3imtr4i	⊢ ( ∃! 𝑦 ∈ 𝑧 ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 → ∃ 𝑤 ∈ 𝑧 ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 )
36	22 35	syl	⊢ ( ( 𝑅 We V ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 )
37		eleq1	⊢ ( ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 → ( ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ 𝑧 ↔ 𝑤 ∈ 𝑧 ) )
38	37	biimparc	⊢ ( ( 𝑤 ∈ 𝑧 ∧ ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 ) → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ 𝑧 )
39	38	rexlimiva	⊢ ( ∃ 𝑤 ∈ 𝑧 ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } = 𝑤 → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ 𝑧 )
40	36 39	syl	⊢ ( ( 𝑅 We V ∧ 𝑧 ≠ ∅ ) → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ 𝑧 )
41	40	elexd	⊢ ( ( 𝑅 We V ∧ 𝑧 ≠ ∅ ) → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ V )
42	14 41	pm2.61dane	⊢ ( 𝑅 We V → ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ V )
43	42	ralrimivw	⊢ ( 𝑅 We V → ∀ 𝑧 ∈ V ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ V )
44	1	fnmpt	⊢ ( ∀ 𝑧 ∈ V ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ V → 𝐹 Fn V )
45	43 44	syl	⊢ ( 𝑅 We V → 𝐹 Fn V )
46	1	fvmpt2	⊢ ( ( 𝑧 ∈ V ∧ ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } ∈ 𝑧 ) → ( 𝐹 ‘ 𝑧 ) = ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } )
47	17 40 46	sylancr	⊢ ( ( 𝑅 We V ∧ 𝑧 ≠ ∅ ) → ( 𝐹 ‘ 𝑧 ) = ∪ { 𝑦 ∈ 𝑧 ∣ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 𝑅 𝑦 } )
48	47 40	eqeltrd	⊢ ( ( 𝑅 We V ∧ 𝑧 ≠ ∅ ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 )
49	48	ex	⊢ ( 𝑅 We V → ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
50	49	alrimiv	⊢ ( 𝑅 We V → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
51	45 50	jca	⊢ ( 𝑅 We V → ( 𝐹 Fn V ∧ ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) ) )