wevgblacfn

Description: If R is a well-ordering of the universe, then G is a global choice function. Here G 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). This is the ZFC version of (3 -> 1) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 29-Jun-2025)

		Ref	Expression
	Hypothesis	wevgblacfn.1	$⊢ G = (z \in V ⟼ ⋃ \{y \in z \| \forall x \in z \neg x R y\})$
	Assertion	wevgblacfn	$⊢ R We V \to (G Fn V \land \forall z (z \neq \emptyset \to G (z) \in z))$

Proof

Step	Hyp	Ref	Expression
1		wevgblacfn.1	$⊢ G = (z \in V ⟼ ⋃ \{y \in z \| \forall x \in z \neg x R y\})$
2		eleq2	$⊢ z = \emptyset \to (y \in z \leftrightarrow y \in \emptyset)$
3		raleq	$⊢ z = \emptyset \to (\forall x \in z \neg x R y \leftrightarrow \forall x \in \emptyset \neg x R y)$
4	2 3	anbi12d	$⊢ z = \emptyset \to ((y \in z \land \forall x \in z \neg x R y) \leftrightarrow (y \in \emptyset \land \forall x \in \emptyset \neg x R y))$
5	4	rabbidva2	$⊢ z = \emptyset \to \{y \in z \| \forall x \in z \neg x R y\} = \{y \in \emptyset \| \forall x \in \emptyset \neg x R y\}$
6	5	unieqd	$⊢ z = \emptyset \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} = ⋃ \{y \in \emptyset \| \forall x \in \emptyset \neg x R y\}$
7		rab0	$⊢ \{y \in \emptyset \| \forall x \in \emptyset \neg x R y\} = \emptyset$
8	7	unieqi	$⊢ ⋃ \{y \in \emptyset \| \forall x \in \emptyset \neg x R y\} = ⋃ \emptyset$
9		uni0	$⊢ ⋃ \emptyset = \emptyset$
10	8 9	eqtri	$⊢ ⋃ \{y \in \emptyset \| \forall x \in \emptyset \neg x R y\} = \emptyset$
11	6 10	eqtrdi	$⊢ z = \emptyset \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} = \emptyset$
12		0ex	$⊢ \emptyset \in V$
13	11 12	eqeltrdi	$⊢ z = \emptyset \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in V$
14	13	adantl	$⊢ (R We V \land z = \emptyset) \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in V$
15		ssv	$⊢ z \subseteq V$
16	15	jctl	$⊢ z \neq \emptyset \to (z \subseteq V \land z \neq \emptyset)$
17		vex	$⊢ z \in V$
18	16 17	jctil	$⊢ z \neq \emptyset \to (z \in V \land (z \subseteq V \land z \neq \emptyset))$
19		3anass	$⊢ (z \in V \land z \subseteq V \land z \neq \emptyset) \leftrightarrow (z \in V \land (z \subseteq V \land z \neq \emptyset))$
20	18 19	sylibr	$⊢ z \neq \emptyset \to (z \in V \land z \subseteq V \land z \neq \emptyset)$
21		wereu	$⊢ (R We V \land (z \in V \land z \subseteq V \land z \neq \emptyset)) \to \exists! y \in z \forall x \in z \neg x R y$
22	20 21	sylan2	$⊢ (R We V \land z \neq \emptyset) \to \exists! y \in z \forall x \in z \neg x R y$
23		vsnid	$⊢ w \in \{w\}$
24		eleq2	$⊢ \{y \in z \| \forall x \in z \neg x R y\} = \{w\} \to (w \in \{y \in z \| \forall x \in z \neg x R y\} \leftrightarrow w \in \{w\})$
25	23 24	mpbiri	$⊢ \{y \in z \| \forall x \in z \neg x R y\} = \{w\} \to w \in \{y \in z \| \forall x \in z \neg x R y\}$
26		elrabi	$⊢ w \in \{y \in z \| \forall x \in z \neg x R y\} \to w \in z$
27	25 26	syl	$⊢ \{y \in z \| \forall x \in z \neg x R y\} = \{w\} \to w \in z$
28		unieq	$⊢ \{y \in z \| \forall x \in z \neg x R y\} = \{w\} \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} = ⋃ \{w\}$
29		unisnv	$⊢ ⋃ \{w\} = w$
30	28 29	eqtrdi	$⊢ \{y \in z \| \forall x \in z \neg x R y\} = \{w\} \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w$
31	27 30	jca	$⊢ \{y \in z \| \forall x \in z \neg x R y\} = \{w\} \to (w \in z \land ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w)$
32	31	eximi	$⊢ \exists w \{y \in z \| \forall x \in z \neg x R y\} = \{w\} \to \exists w (w \in z \land ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w)$
33		reusn	$⊢ \exists! y \in z \forall x \in z \neg x R y \leftrightarrow \exists w \{y \in z \| \forall x \in z \neg x R y\} = \{w\}$
34		df-rex	$⊢ \exists w \in z ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w \leftrightarrow \exists w (w \in z \land ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w)$
35	32 33 34	3imtr4i	$⊢ \exists! y \in z \forall x \in z \neg x R y \to \exists w \in z ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w$
36	22 35	syl	$⊢ (R We V \land z \neq \emptyset) \to \exists w \in z ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w$
37		eleq1	$⊢ ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w \to (⋃ \{y \in z \| \forall x \in z \neg x R y\} \in z \leftrightarrow w \in z)$
38	37	biimparc	$⊢ (w \in z \land ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w) \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in z$
39	38	rexlimiva	$⊢ \exists w \in z ⋃ \{y \in z \| \forall x \in z \neg x R y\} = w \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in z$
40	36 39	syl	$⊢ (R We V \land z \neq \emptyset) \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in z$
41	40	elexd	$⊢ (R We V \land z \neq \emptyset) \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in V$
42	14 41	pm2.61dane	$⊢ R We V \to ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in V$
43	42	ralrimivw	$⊢ R We V \to \forall z \in V ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in V$
44	1	fnmpt	$⊢ \forall z \in V ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in V \to G Fn V$
45	43 44	syl	$⊢ R We V \to G Fn V$
46	1	fvmpt2	$⊢ (z \in V \land ⋃ \{y \in z \| \forall x \in z \neg x R y\} \in z) \to G (z) = ⋃ \{y \in z \| \forall x \in z \neg x R y\}$
47	17 40 46	sylancr	$⊢ (R We V \land z \neq \emptyset) \to G (z) = ⋃ \{y \in z \| \forall x \in z \neg x R y\}$
48	47 40	eqeltrd	$⊢ (R We V \land z \neq \emptyset) \to G (z) \in z$
49	48	ex	$⊢ R We V \to (z \neq \emptyset \to G (z) \in z)$
50	49	alrimiv	$⊢ R We V \to \forall z (z \neq \emptyset \to G (z) \in z)$
51	45 50	jca	$⊢ R We V \to (G Fn V \land \forall z (z \neq \emptyset \to G (z) \in z))$

Metamath Proof Explorer

Theorem wevgblacfn

Proof