vonf1oonfo

Description: If F is a bijection from the ordinals to the universe and A is non-empty, then H maps the ordinals onto A . This is the ZFC version of (5 -> 8) in https://tinyurl.com/hamkins-gblac , though it neglects to specify that A must be non-empty. Note that in NBG set theory the antecedent would be something like A. X ( -. X e.V -> E. F F : X -1-1-onto-> On ) , but since we cannot quantify over classes, we instead consider only the case X = V which is sufficient for this proof. This theorem can also be viewed as (2 -> 8). (Contributed by BTernaryTau, 11-Jun-2026)

	Ref	Expression
Hypotheses	vonf1oonfo.1	$⊢ H = (x \in On ⟼ if (F (x) \in A, F (x), D))$
	vonf1oonfo.2	$⊢ D = F (⋂ \{y \in On \| F (y) \in A\})$
Assertion	vonf1oonfo	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to H : On \underset{onto}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		vonf1oonfo.1	$⊢ H = (x \in On ⟼ if (F (x) \in A, F (x), D))$
2		vonf1oonfo.2	$⊢ D = F (⋂ \{y \in On \| F (y) \in A\})$
3	1	rnmpt	$⊢ ran H = \{z \| \exists x \in On z = if (F (x) \in A, F (x), D)\}$
4		iffalse	$⊢ \neg F (x) \in A \to if (F (x) \in A, F (x), D) = D$
5	4	3ad2ant3	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset \land \neg F (x) \in A) \to if (F (x) \in A, F (x), D) = D$
6		n0	$⊢ A \neq \emptyset \leftrightarrow \exists w w \in A$
7		19.42v	$⊢ \exists w (F : On \underset{1-1 onto}{⟶} V \land w \in A) \leftrightarrow (F : On \underset{1-1 onto}{⟶} V \land \exists w w \in A)$
8		f1ofo	$⊢ F : On \underset{1-1 onto}{⟶} V \to F : On \underset{onto}{⟶} V$
9		foelcdmi	$⊢ (F : On \underset{onto}{⟶} V \land w \in V) \to \exists y \in On F (y) = w$
10	9	elvd	$⊢ F : On \underset{onto}{⟶} V \to \exists y \in On F (y) = w$
11	8 10	syl	$⊢ F : On \underset{1-1 onto}{⟶} V \to \exists y \in On F (y) = w$
12		r19.41v	$⊢ \exists y \in On (F (y) = w \land w \in A) \leftrightarrow (\exists y \in On F (y) = w \land w \in A)$
13		eleq1	$⊢ F (y) = w \to (F (y) \in A \leftrightarrow w \in A)$
14	13	biimpar	$⊢ (F (y) = w \land w \in A) \to F (y) \in A$
15	14	reximi	$⊢ \exists y \in On (F (y) = w \land w \in A) \to \exists y \in On F (y) \in A$
16	12 15	sylbir	$⊢ (\exists y \in On F (y) = w \land w \in A) \to \exists y \in On F (y) \in A$
17	11 16	sylan	$⊢ (F : On \underset{1-1 onto}{⟶} V \land w \in A) \to \exists y \in On F (y) \in A$
18	17	exlimiv	$⊢ \exists w (F : On \underset{1-1 onto}{⟶} V \land w \in A) \to \exists y \in On F (y) \in A$
19	7 18	sylbir	$⊢ (F : On \underset{1-1 onto}{⟶} V \land \exists w w \in A) \to \exists y \in On F (y) \in A$
20	6 19	sylan2b	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to \exists y \in On F (y) \in A$
21		nfcv	$⊢ \underline{Ⅎ} y F$
22		nfrab1	$⊢ \underline{Ⅎ} y \{y \in On \| F (y) \in A\}$
23	22	nfint	$⊢ \underline{Ⅎ} y ⋂ \{y \in On \| F (y) \in A\}$
24	21 23	nffv	$⊢ \underline{Ⅎ} y F (⋂ \{y \in On \| F (y) \in A\})$
25	24	nfel1	$⊢ Ⅎ y F (⋂ \{y \in On \| F (y) \in A\}) \in A$
26		fveq2	$⊢ y = ⋂ \{y \in On \| F (y) \in A\} \to F (y) = F (⋂ \{y \in On \| F (y) \in A\})$
27	26	eleq1d	$⊢ y = ⋂ \{y \in On \| F (y) \in A\} \to (F (y) \in A \leftrightarrow F (⋂ \{y \in On \| F (y) \in A\}) \in A)$
28	25 27	onminsb	$⊢ \exists y \in On F (y) \in A \to F (⋂ \{y \in On \| F (y) \in A\}) \in A$
29	2 28	eqeltrid	$⊢ \exists y \in On F (y) \in A \to D \in A$
30	20 29	syl	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to D \in A$
31	30	3adant3	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset \land \neg F (x) \in A) \to D \in A$
32	5 31	eqeltrd	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset \land \neg F (x) \in A) \to if (F (x) \in A, F (x), D) \in A$
33	32	3expia	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to (\neg F (x) \in A \to if (F (x) \in A, F (x), D) \in A)$
34		iftrue	$⊢ F (x) \in A \to if (F (x) \in A, F (x), D) = F (x)$
35		id	$⊢ F (x) \in A \to F (x) \in A$
36	34 35	eqeltrd	$⊢ F (x) \in A \to if (F (x) \in A, F (x), D) \in A$
37	33 36	pm2.61d2	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to if (F (x) \in A, F (x), D) \in A$
38		eleq1	$⊢ z = if (F (x) \in A, F (x), D) \to (z \in A \leftrightarrow if (F (x) \in A, F (x), D) \in A)$
39	37 38	syl5ibrcom	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to (z = if (F (x) \in A, F (x), D) \to z \in A)$
40	39	rexlimdvw	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to (\exists x \in On z = if (F (x) \in A, F (x), D) \to z \in A)$
41	40	abssdv	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to \{z \| \exists x \in On z = if (F (x) \in A, F (x), D)\} \subseteq A$
42	3 41	eqsstrid	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to ran H \subseteq A$
43		fveqeq2	$⊢ x = F^{-1} (z) \to (F (x) = z \leftrightarrow F (F^{-1} (z)) = z)$
44		f1ocnvdm	$⊢ (F : On \underset{1-1 onto}{⟶} V \land z \in V) \to F^{-1} (z) \in On$
45	44	elvd	$⊢ F : On \underset{1-1 onto}{⟶} V \to F^{-1} (z) \in On$
46		f1ocnvfv2	$⊢ (F : On \underset{1-1 onto}{⟶} V \land z \in V) \to F (F^{-1} (z)) = z$
47	46	elvd	$⊢ F : On \underset{1-1 onto}{⟶} V \to F (F^{-1} (z)) = z$
48	43 45 47	rspcedvdw	$⊢ F : On \underset{1-1 onto}{⟶} V \to \exists x \in On F (x) = z$
49		eleq1	$⊢ F (x) = z \to (F (x) \in A \leftrightarrow z \in A)$
50	49	biimpar	$⊢ (F (x) = z \land z \in A) \to F (x) \in A$
51	50	iftrued	$⊢ (F (x) = z \land z \in A) \to if (F (x) \in A, F (x), D) = F (x)$
52		simpl	$⊢ (F (x) = z \land z \in A) \to F (x) = z$
53	51 52	eqtr2d	$⊢ (F (x) = z \land z \in A) \to z = if (F (x) \in A, F (x), D)$
54	53	expcom	$⊢ z \in A \to (F (x) = z \to z = if (F (x) \in A, F (x), D))$
55	54	reximdv	$⊢ z \in A \to (\exists x \in On F (x) = z \to \exists x \in On z = if (F (x) \in A, F (x), D))$
56	48 55	syl5com	$⊢ F : On \underset{1-1 onto}{⟶} V \to (z \in A \to \exists x \in On z = if (F (x) \in A, F (x), D))$
57	56	ralrimiv	$⊢ F : On \underset{1-1 onto}{⟶} V \to \forall z \in A \exists x \in On z = if (F (x) \in A, F (x), D)$
58		ssabral	$⊢ A \subseteq \{z \| \exists x \in On z = if (F (x) \in A, F (x), D)\} \leftrightarrow \forall z \in A \exists x \in On z = if (F (x) \in A, F (x), D)$
59	57 58	sylibr	$⊢ F : On \underset{1-1 onto}{⟶} V \to A \subseteq \{z \| \exists x \in On z = if (F (x) \in A, F (x), D)\}$
60	59 3	sseqtrrdi	$⊢ F : On \underset{1-1 onto}{⟶} V \to A \subseteq ran H$
61	60	adantr	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to A \subseteq ran H$
62	42 61	eqssd	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to ran H = A$
63		fvex	$⊢ F (x) \in V$
64	2	fvexi	$⊢ D \in V$
65	63 64	ifex	$⊢ if (F (x) \in A, F (x), D) \in V$
66	65 1	fnmpti	$⊢ H Fn On$
67		df-fo	$⊢ H : On \underset{onto}{⟶} A \leftrightarrow (H Fn On \land ran H = A)$
68	66 67	mpbiran	$⊢ H : On \underset{onto}{⟶} A \leftrightarrow ran H = A$
69	62 68	sylibr	$⊢ (F : On \underset{1-1 onto}{⟶} V \land A \neq \emptyset) \to H : On \underset{onto}{⟶} A$

Metamath Proof Explorer

Theorem vonf1oonfo

Proof