vonf1owev

Description: If F is a bijection from the universe to the ordinals, then R well-orders the universe. This is the ZFC version of (2 -> 3) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 6-Dec-2025)

		Ref	Expression
	Hypothesis	vonf1owev.1	$⊢ R = \{⟨x, y⟩ \| F (x) \in F (y)\}$
	Assertion	vonf1owev	$⊢ F : V \underset{1-1 onto}{⟶} On \to R We V$

Proof

Step	Hyp	Ref	Expression
1		vonf1owev.1	$⊢ R = \{⟨x, y⟩ \| F (x) \in F (y)\}$
2		f1of	$⊢ F : V \underset{1-1 onto}{⟶} On \to F : V ⟶ On$
3	2	fimassd	$⊢ F : V \underset{1-1 onto}{⟶} On \to F [t] \subseteq On$
4		f1odm	$⊢ F : V \underset{1-1 onto}{⟶} On \to dom F = V$
5	4	ineq1d	$⊢ F : V \underset{1-1 onto}{⟶} On \to dom F \cap t = V \cap t$
6	5	neeq1d	$⊢ F : V \underset{1-1 onto}{⟶} On \to (dom F \cap t \neq \emptyset \leftrightarrow V \cap t \neq \emptyset)$
7		inv1	$⊢ t \cap V = t$
8	7	ineqcomi	$⊢ V \cap t = t$
9	8	neeq1i	$⊢ V \cap t \neq \emptyset \leftrightarrow t \neq \emptyset$
10	6 9	bitr2di	$⊢ F : V \underset{1-1 onto}{⟶} On \to (t \neq \emptyset \leftrightarrow dom F \cap t \neq \emptyset)$
11	10	biimpa	$⊢ (F : V \underset{1-1 onto}{⟶} On \land t \neq \emptyset) \to dom F \cap t \neq \emptyset$
12	11	imadisjlnd	$⊢ (F : V \underset{1-1 onto}{⟶} On \land t \neq \emptyset) \to F [t] \neq \emptyset$
13		onssmin	$⊢ (F [t] \subseteq On \land F [t] \neq \emptyset) \to \exists r \in F [t] \forall s \in F [t] r \subseteq s$
14	3 12 13	syl2an2r	$⊢ (F : V \underset{1-1 onto}{⟶} On \land t \neq \emptyset) \to \exists r \in F [t] \forall s \in F [t] r \subseteq s$
15	14	ex	$⊢ F : V \underset{1-1 onto}{⟶} On \to (t \neq \emptyset \to \exists r \in F [t] \forall s \in F [t] r \subseteq s)$
16		vex	$⊢ v \in V$
17		vex	$⊢ u \in V$
18		fveq2	$⊢ x = v \to F (x) = F (v)$
19	18	eleq1d	$⊢ x = v \to (F (x) \in F (y) \leftrightarrow F (v) \in F (y))$
20		fveq2	$⊢ y = u \to F (y) = F (u)$
21	20	eleq2d	$⊢ y = u \to (F (v) \in F (y) \leftrightarrow F (v) \in F (u))$
22	16 17 19 21 1	brab	$⊢ v R u \leftrightarrow F (v) \in F (u)$
23	22	notbii	$⊢ \neg v R u \leftrightarrow \neg F (v) \in F (u)$
24	2	ffvelcdmda	$⊢ (F : V \underset{1-1 onto}{⟶} On \land u \in V) \to F (u) \in On$
25	24	elvd	$⊢ F : V \underset{1-1 onto}{⟶} On \to F (u) \in On$
26	2	ffvelcdmda	$⊢ (F : V \underset{1-1 onto}{⟶} On \land v \in V) \to F (v) \in On$
27	26	elvd	$⊢ F : V \underset{1-1 onto}{⟶} On \to F (v) \in On$
28		ontri1	$⊢ (F (u) \in On \land F (v) \in On) \to (F (u) \subseteq F (v) \leftrightarrow \neg F (v) \in F (u))$
29	25 27 28	syl2anc	$⊢ F : V \underset{1-1 onto}{⟶} On \to (F (u) \subseteq F (v) \leftrightarrow \neg F (v) \in F (u))$
30	23 29	bitr4id	$⊢ F : V \underset{1-1 onto}{⟶} On \to (\neg v R u \leftrightarrow F (u) \subseteq F (v))$
31	30	ralbidv	$⊢ F : V \underset{1-1 onto}{⟶} On \to (\forall v \in t \neg v R u \leftrightarrow \forall v \in t F (u) \subseteq F (v))$
32		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} On \to F Fn V$
33		ssv	$⊢ t \subseteq V$
34		sseq2	$⊢ s = F (v) \to (F (u) \subseteq s \leftrightarrow F (u) \subseteq F (v))$
35	34	ralima	$⊢ (F Fn V \land t \subseteq V) \to (\forall s \in F [t] F (u) \subseteq s \leftrightarrow \forall v \in t F (u) \subseteq F (v))$
36	32 33 35	sylancl	$⊢ F : V \underset{1-1 onto}{⟶} On \to (\forall s \in F [t] F (u) \subseteq s \leftrightarrow \forall v \in t F (u) \subseteq F (v))$
37	31 36	bitr4d	$⊢ F : V \underset{1-1 onto}{⟶} On \to (\forall v \in t \neg v R u \leftrightarrow \forall s \in F [t] F (u) \subseteq s)$
38	37	rexbidv	$⊢ F : V \underset{1-1 onto}{⟶} On \to (\exists u \in t \forall v \in t \neg v R u \leftrightarrow \exists u \in t \forall s \in F [t] F (u) \subseteq s)$
39		sseq1	$⊢ r = F (u) \to (r \subseteq s \leftrightarrow F (u) \subseteq s)$
40	39	ralbidv	$⊢ r = F (u) \to (\forall s \in F [t] r \subseteq s \leftrightarrow \forall s \in F [t] F (u) \subseteq s)$
41	40	rexima	$⊢ (F Fn V \land t \subseteq V) \to (\exists r \in F [t] \forall s \in F [t] r \subseteq s \leftrightarrow \exists u \in t \forall s \in F [t] F (u) \subseteq s)$
42	32 33 41	sylancl	$⊢ F : V \underset{1-1 onto}{⟶} On \to (\exists r \in F [t] \forall s \in F [t] r \subseteq s \leftrightarrow \exists u \in t \forall s \in F [t] F (u) \subseteq s)$
43	38 42	bitr4d	$⊢ F : V \underset{1-1 onto}{⟶} On \to (\exists u \in t \forall v \in t \neg v R u \leftrightarrow \exists r \in F [t] \forall s \in F [t] r \subseteq s)$
44	15 43	sylibrd	$⊢ F : V \underset{1-1 onto}{⟶} On \to (t \neq \emptyset \to \exists u \in t \forall v \in t \neg v R u)$
45	44	alrimiv	$⊢ F : V \underset{1-1 onto}{⟶} On \to \forall t (t \neq \emptyset \to \exists u \in t \forall v \in t \neg v R u)$
46		df-fr	$⊢ R Fr V \leftrightarrow \forall t ((t \subseteq V \land t \neq \emptyset) \to \exists u \in t \forall v \in t \neg v R u)$
47	33	biantrur	$⊢ t \neq \emptyset \leftrightarrow (t \subseteq V \land t \neq \emptyset)$
48	47	imbi1i	$⊢ (t \neq \emptyset \to \exists u \in t \forall v \in t \neg v R u) \leftrightarrow ((t \subseteq V \land t \neq \emptyset) \to \exists u \in t \forall v \in t \neg v R u)$
49	48	albii	$⊢ \forall t (t \neq \emptyset \to \exists u \in t \forall v \in t \neg v R u) \leftrightarrow \forall t ((t \subseteq V \land t \neq \emptyset) \to \exists u \in t \forall v \in t \neg v R u)$
50	46 49	bitr4i	$⊢ R Fr V \leftrightarrow \forall t (t \neq \emptyset \to \exists u \in t \forall v \in t \neg v R u)$
51	45 50	sylibr	$⊢ F : V \underset{1-1 onto}{⟶} On \to R Fr V$
52	2	ffvelcdmda	$⊢ (F : V \underset{1-1 onto}{⟶} On \land w \in V) \to F (w) \in On$
53	52	elvd	$⊢ F : V \underset{1-1 onto}{⟶} On \to F (w) \in On$
54	2	ffvelcdmda	$⊢ (F : V \underset{1-1 onto}{⟶} On \land z \in V) \to F (z) \in On$
55	54	elvd	$⊢ F : V \underset{1-1 onto}{⟶} On \to F (z) \in On$
56		oneltri	$⊢ (F (w) \in On \land F (z) \in On) \to (F (w) \in F (z) \lor F (z) \in F (w) \lor F (w) = F (z))$
57	53 55 56	syl2anc	$⊢ F : V \underset{1-1 onto}{⟶} On \to (F (w) \in F (z) \lor F (z) \in F (w) \lor F (w) = F (z))$
58		3orcomb	$⊢ (F (w) \in F (z) \lor F (z) \in F (w) \lor F (w) = F (z)) \leftrightarrow (F (w) \in F (z) \lor F (w) = F (z) \lor F (z) \in F (w))$
59	57 58	sylib	$⊢ F : V \underset{1-1 onto}{⟶} On \to (F (w) \in F (z) \lor F (w) = F (z) \lor F (z) \in F (w))$
60		vex	$⊢ w \in V$
61		vex	$⊢ z \in V$
62		fveq2	$⊢ x = w \to F (x) = F (w)$
63	62	eleq1d	$⊢ x = w \to (F (x) \in F (y) \leftrightarrow F (w) \in F (y))$
64		fveq2	$⊢ y = z \to F (y) = F (z)$
65	64	eleq2d	$⊢ y = z \to (F (w) \in F (y) \leftrightarrow F (w) \in F (z))$
66	60 61 63 65 1	brab	$⊢ w R z \leftrightarrow F (w) \in F (z)$
67	66	biimpri	$⊢ F (w) \in F (z) \to w R z$
68	67	a1i	$⊢ F : V \underset{1-1 onto}{⟶} On \to (F (w) \in F (z) \to w R z)$
69		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} On \to F : V \underset{1-1}{⟶} On$
70		f1veqaeq	$⊢ (F : V \underset{1-1}{⟶} On \land (w \in V \land z \in V)) \to (F (w) = F (z) \to w = z)$
71	60 61 70	mpanr12	$⊢ F : V \underset{1-1}{⟶} On \to (F (w) = F (z) \to w = z)$
72	69 71	syl	$⊢ F : V \underset{1-1 onto}{⟶} On \to (F (w) = F (z) \to w = z)$
73		fveq2	$⊢ x = z \to F (x) = F (z)$
74	73	eleq1d	$⊢ x = z \to (F (x) \in F (y) \leftrightarrow F (z) \in F (y))$
75		fveq2	$⊢ y = w \to F (y) = F (w)$
76	75	eleq2d	$⊢ y = w \to (F (z) \in F (y) \leftrightarrow F (z) \in F (w))$
77	61 60 74 76 1	brab	$⊢ z R w \leftrightarrow F (z) \in F (w)$
78	77	biimpri	$⊢ F (z) \in F (w) \to z R w$
79	78	a1i	$⊢ F : V \underset{1-1 onto}{⟶} On \to (F (z) \in F (w) \to z R w)$
80	68 72 79	3orim123d	$⊢ F : V \underset{1-1 onto}{⟶} On \to ((F (w) \in F (z) \lor F (w) = F (z) \lor F (z) \in F (w)) \to (w R z \lor w = z \lor z R w))$
81	59 80	mpd	$⊢ F : V \underset{1-1 onto}{⟶} On \to (w R z \lor w = z \lor z R w)$
82	81	ralrimivw	$⊢ F : V \underset{1-1 onto}{⟶} On \to \forall z \in V (w R z \lor w = z \lor z R w)$
83	82	ralrimivw	$⊢ F : V \underset{1-1 onto}{⟶} On \to \forall w \in V \forall z \in V (w R z \lor w = z \lor z R w)$
84		dfwe2	$⊢ R We V \leftrightarrow (R Fr V \land \forall w \in V \forall z \in V (w R z \lor w = z \lor z R w))$
85	51 83 84	sylanbrc	$⊢ F : V \underset{1-1 onto}{⟶} On \to R We V$

Metamath Proof Explorer

Theorem vonf1owev

Proof