Theorem permac8prim

Description: The Axiom of Choice ac8prim holds in permutation models. Part of Exercise II.9.3 of Kunen2 p. 149. Note that ax-ac requires Regularity for its derivation from the usual Axiom of Choice and does not necessarily hold in permutation models. (Contributed by Eric Schmidt, 16-Nov-2025)

	Ref	Expression
Hypotheses	permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
	permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
Assertion	permac8prim	$$⊢\left(\forall z\left(zRx\to \exists wwRz\right)\wedge \forall z\forall w\left(\left(zRx\wedge wRx\right)\to \left(\neg z=w\to \forall y\left(yRz\to \neg yRw\right)\right)\right)\right)\to \exists y\forall z\left(zRx\to \exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
3		df-ral	$$⊢\forall z\in F\left(x\right)F\left(z\right)\ne \varnothing \leftrightarrow \forall z\left(z\in F\left(x\right)\to F\left(z\right)\ne \varnothing \right)$$
4		f1ofn	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\to FFn\mathrm{V}$$
5	1 4	ax-mp	$$⊢FFn\mathrm{V}$$
6		ssv	$$⊢F\left(x\right)\subseteq \mathrm{V}$$
7		neeq1	$$⊢t=F\left(z\right)\to \left(t\ne \varnothing \leftrightarrow F\left(z\right)\ne \varnothing \right)$$
8	7	ralima	$$⊢\left(FFn\mathrm{V}\wedge F\left(x\right)\subseteq \mathrm{V}\right)\to \left(\forall t\in F\left[F\left(x\right)\right]t\ne \varnothing \leftrightarrow \forall z\in F\left(x\right)F\left(z\right)\ne \varnothing \right)$$
9	5 6 8	mp2an	$$⊢\forall t\in F\left[F\left(x\right)\right]t\ne \varnothing \leftrightarrow \forall z\in F\left(x\right)F\left(z\right)\ne \varnothing$$
10		vex	$$⊢z\in \mathrm{V}$$
11		vex	$$⊢x\in \mathrm{V}$$
12	1 2 10 11	brpermmodel	$$⊢zRx\leftrightarrow z\in F\left(x\right)$$
13		vex	$$⊢w\in \mathrm{V}$$
14	1 2 13 10	brpermmodel	$$⊢wRz\leftrightarrow w\in F\left(z\right)$$
15	14	exbii	$$⊢\exists wwRz\leftrightarrow \exists ww\in F\left(z\right)$$
16		n0	$$⊢F\left(z\right)\ne \varnothing \leftrightarrow \exists ww\in F\left(z\right)$$
17	15 16	bitr4i	$$⊢\exists wwRz\leftrightarrow F\left(z\right)\ne \varnothing$$
18	12 17	imbi12i	$$⊢\left(zRx\to \exists wwRz\right)\leftrightarrow \left(z\in F\left(x\right)\to F\left(z\right)\ne \varnothing \right)$$
19	18	albii	$$⊢\forall z\left(zRx\to \exists wwRz\right)\leftrightarrow \forall z\left(z\in F\left(x\right)\to F\left(z\right)\ne \varnothing \right)$$
20	3 9 19	3bitr4i	$$⊢\forall t\in F\left[F\left(x\right)\right]t\ne \varnothing \leftrightarrow \forall z\left(zRx\to \exists wwRz\right)$$
21		neeq2	$$⊢q=F\left(w\right)\to \left(t\ne q\leftrightarrow t\ne F\left(w\right)\right)$$
22		ineq2	$$⊢q=F\left(w\right)\to t\cap q=t\cap F\left(w\right)$$
23	22	eqeq1d	$$⊢q=F\left(w\right)\to \left(t\cap q=\varnothing \leftrightarrow t\cap F\left(w\right)=\varnothing \right)$$
24	21 23	imbi12d	$$⊢q=F\left(w\right)\to \left(\left(t\ne q\to t\cap q=\varnothing \right)\leftrightarrow \left(t\ne F\left(w\right)\to t\cap F\left(w\right)=\varnothing \right)\right)$$
25	24	ralima	$$⊢\left(FFn\mathrm{V}\wedge F\left(x\right)\subseteq \mathrm{V}\right)\to \left(\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\leftrightarrow \forall w\in F\left(x\right)\left(t\ne F\left(w\right)\to t\cap F\left(w\right)=\varnothing \right)\right)$$
26	5 6 25	mp2an	$$⊢\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\leftrightarrow \forall w\in F\left(x\right)\left(t\ne F\left(w\right)\to t\cap F\left(w\right)=\varnothing \right)$$
27	26	ralbii	$$⊢\forall t\in F\left[F\left(x\right)\right]\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\leftrightarrow \forall t\in F\left[F\left(x\right)\right]\forall w\in F\left(x\right)\left(t\ne F\left(w\right)\to t\cap F\left(w\right)=\varnothing \right)$$
28		neeq1	$$⊢t=F\left(z\right)\to \left(t\ne F\left(w\right)\leftrightarrow F\left(z\right)\ne F\left(w\right)\right)$$
29		ineq1	$$⊢t=F\left(z\right)\to t\cap F\left(w\right)=F\left(z\right)\cap F\left(w\right)$$
30	29	eqeq1d	$$⊢t=F\left(z\right)\to \left(t\cap F\left(w\right)=\varnothing \leftrightarrow F\left(z\right)\cap F\left(w\right)=\varnothing \right)$$
31	28 30	imbi12d	$$⊢t=F\left(z\right)\to \left(\left(t\ne F\left(w\right)\to t\cap F\left(w\right)=\varnothing \right)\leftrightarrow \left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)\right)$$
32	31	ralbidv	$$⊢t=F\left(z\right)\to \left(\forall w\in F\left(x\right)\left(t\ne F\left(w\right)\to t\cap F\left(w\right)=\varnothing \right)\leftrightarrow \forall w\in F\left(x\right)\left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)\right)$$
33	32	ralima	$$⊢\left(FFn\mathrm{V}\wedge F\left(x\right)\subseteq \mathrm{V}\right)\to \left(\forall t\in F\left[F\left(x\right)\right]\forall w\in F\left(x\right)\left(t\ne F\left(w\right)\to t\cap F\left(w\right)=\varnothing \right)\leftrightarrow \forall z\in F\left(x\right)\forall w\in F\left(x\right)\left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)\right)$$
34	5 6 33	mp2an	$$⊢\forall t\in F\left[F\left(x\right)\right]\forall w\in F\left(x\right)\left(t\ne F\left(w\right)\to t\cap F\left(w\right)=\varnothing \right)\leftrightarrow \forall z\in F\left(x\right)\forall w\in F\left(x\right)\left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)$$
35		r2al	$$⊢\forall z\in F\left(x\right)\forall w\in F\left(x\right)\left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)\leftrightarrow \forall z\forall w\left(\left(z\in F\left(x\right)\wedge w\in F\left(x\right)\right)\to \left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)\right)$$
36	27 34 35	3bitri	$$⊢\forall t\in F\left[F\left(x\right)\right]\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\leftrightarrow \forall z\forall w\left(\left(z\in F\left(x\right)\wedge w\in F\left(x\right)\right)\to \left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)\right)$$
37	1 2 13 11	brpermmodel	$$⊢wRx\leftrightarrow w\in F\left(x\right)$$
38	12 37	anbi12i	$$⊢\left(zRx\wedge wRx\right)\leftrightarrow \left(z\in F\left(x\right)\wedge w\in F\left(x\right)\right)$$
39		df-ne	$$⊢F\left(z\right)\ne F\left(w\right)\leftrightarrow \neg F\left(z\right)=F\left(w\right)$$
40		f1of1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\to F:\mathrm{V}\underset{1-1}{⟶}\mathrm{V}$$
41	1 40	ax-mp	$$⊢F:\mathrm{V}\underset{1-1}{⟶}\mathrm{V}$$
42		f1fveq	$$⊢\left(F:\mathrm{V}\underset{1-1}{⟶}\mathrm{V}\wedge \left(z\in \mathrm{V}\wedge w\in \mathrm{V}\right)\right)\to \left(F\left(z\right)=F\left(w\right)\leftrightarrow z=w\right)$$
43	41 42	mpan	$$⊢\left(z\in \mathrm{V}\wedge w\in \mathrm{V}\right)\to \left(F\left(z\right)=F\left(w\right)\leftrightarrow z=w\right)$$
44	43	el2v	$$⊢F\left(z\right)=F\left(w\right)\leftrightarrow z=w$$
45	44	notbii	$$⊢\neg F\left(z\right)=F\left(w\right)\leftrightarrow \neg z=w$$
46	39 45	bitr2i	$$⊢\neg z=w\leftrightarrow F\left(z\right)\ne F\left(w\right)$$
47		vex	$$⊢y\in \mathrm{V}$$
48	1 2 47 10	brpermmodel	$$⊢yRz\leftrightarrow y\in F\left(z\right)$$
49	1 2 47 13	brpermmodel	$$⊢yRw\leftrightarrow y\in F\left(w\right)$$
50	49	notbii	$$⊢\neg yRw\leftrightarrow \neg y\in F\left(w\right)$$
51	48 50	imbi12i	$$⊢\left(yRz\to \neg yRw\right)\leftrightarrow \left(y\in F\left(z\right)\to \neg y\in F\left(w\right)\right)$$
52	51	albii	$$⊢\forall y\left(yRz\to \neg yRw\right)\leftrightarrow \forall y\left(y\in F\left(z\right)\to \neg y\in F\left(w\right)\right)$$
53		disj1	$$⊢F\left(z\right)\cap F\left(w\right)=\varnothing \leftrightarrow \forall y\left(y\in F\left(z\right)\to \neg y\in F\left(w\right)\right)$$
54	52 53	bitr4i	$$⊢\forall y\left(yRz\to \neg yRw\right)\leftrightarrow F\left(z\right)\cap F\left(w\right)=\varnothing$$
55	46 54	imbi12i	$$⊢\left(\neg z=w\to \forall y\left(yRz\to \neg yRw\right)\right)\leftrightarrow \left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)$$
56	38 55	imbi12i	$$⊢\left(\left(zRx\wedge wRx\right)\to \left(\neg z=w\to \forall y\left(yRz\to \neg yRw\right)\right)\right)\leftrightarrow \left(\left(z\in F\left(x\right)\wedge w\in F\left(x\right)\right)\to \left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)\right)$$
57	56	2albii	$$⊢\forall z\forall w\left(\left(zRx\wedge wRx\right)\to \left(\neg z=w\to \forall y\left(yRz\to \neg yRw\right)\right)\right)\leftrightarrow \forall z\forall w\left(\left(z\in F\left(x\right)\wedge w\in F\left(x\right)\right)\to \left(F\left(z\right)\ne F\left(w\right)\to F\left(z\right)\cap F\left(w\right)=\varnothing \right)\right)$$
58	36 57	bitr4i	$$⊢\forall t\in F\left[F\left(x\right)\right]\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\leftrightarrow \forall z\forall w\left(\left(zRx\wedge wRx\right)\to \left(\neg z=w\to \forall y\left(yRz\to \neg yRw\right)\right)\right)$$
59		f1ofun	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\to \mathrm{Fun}F$$
60		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
61	60	funimaex	$$⊢\mathrm{Fun}F\to F\left[F\left(x\right)\right]\in \mathrm{V}$$
62	1 59 61	mp2b	$$⊢F\left[F\left(x\right)\right]\in \mathrm{V}$$
63		raleq	$$⊢r=F\left[F\left(x\right)\right]\to \left(\forall t\in rt\ne \varnothing \leftrightarrow \forall t\in F\left[F\left(x\right)\right]t\ne \varnothing \right)$$
64		raleq	$$⊢r=F\left[F\left(x\right)\right]\to \left(\forall q\in r\left(t\ne q\to t\cap q=\varnothing \right)\leftrightarrow \forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\right)$$
65	64	raleqbi1dv	$$⊢r=F\left[F\left(x\right)\right]\to \left(\forall t\in r\forall q\in r\left(t\ne q\to t\cap q=\varnothing \right)\leftrightarrow \forall t\in F\left[F\left(x\right)\right]\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\right)$$
66	63 65	anbi12d	$$⊢r=F\left[F\left(x\right)\right]\to \left(\left(\forall t\in rt\ne \varnothing \wedge \forall t\in r\forall q\in r\left(t\ne q\to t\cap q=\varnothing \right)\right)\leftrightarrow \left(\forall t\in F\left[F\left(x\right)\right]t\ne \varnothing \wedge \forall t\in F\left[F\left(x\right)\right]\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\right)\right)$$
67		raleq	$$⊢r=F\left[F\left(x\right)\right]\to \left(\forall t\in r\exists !vv\in \left(t\cap s\right)\leftrightarrow \forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)\right)$$
68	67	exbidv	$$⊢r=F\left[F\left(x\right)\right]\to \left(\exists s\forall t\in r\exists !vv\in \left(t\cap s\right)\leftrightarrow \exists s\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)\right)$$
69	66 68	imbi12d	$$⊢r=F\left[F\left(x\right)\right]\to \left(\left(\left(\forall t\in rt\ne \varnothing \wedge \forall t\in r\forall q\in r\left(t\ne q\to t\cap q=\varnothing \right)\right)\to \exists s\forall t\in r\exists !vv\in \left(t\cap s\right)\right)\leftrightarrow \left(\left(\forall t\in F\left[F\left(x\right)\right]t\ne \varnothing \wedge \forall t\in F\left[F\left(x\right)\right]\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\right)\to \exists s\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)\right)\right)$$
70		ac8	$$⊢\left(\forall t\in rt\ne \varnothing \wedge \forall t\in r\forall q\in r\left(t\ne q\to t\cap q=\varnothing \right)\right)\to \exists s\forall t\in r\exists !vv\in \left(t\cap s\right)$$
71	62 69 70	vtocl	$$⊢\left(\forall t\in F\left[F\left(x\right)\right]t\ne \varnothing \wedge \forall t\in F\left[F\left(x\right)\right]\forall q\in F\left[F\left(x\right)\right]\left(t\ne q\to t\cap q=\varnothing \right)\right)\to \exists s\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)$$
72	20 58 71	syl2anbr	$$⊢\left(\forall z\left(zRx\to \exists wwRz\right)\wedge \forall z\forall w\left(\left(zRx\wedge wRx\right)\to \left(\neg z=w\to \forall y\left(yRz\to \neg yRw\right)\right)\right)\right)\to \exists s\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)$$
73		ineq1	$$⊢t=F\left(z\right)\to t\cap s=F\left(z\right)\cap s$$
74	73	eleq2d	$$⊢t=F\left(z\right)\to \left(v\in \left(t\cap s\right)\leftrightarrow v\in \left(F\left(z\right)\cap s\right)\right)$$
75	74	eubidv	$$⊢t=F\left(z\right)\to \left(\exists !vv\in \left(t\cap s\right)\leftrightarrow \exists !vv\in \left(F\left(z\right)\cap s\right)\right)$$
76	75	ralima	$$⊢\left(FFn\mathrm{V}\wedge F\left(x\right)\subseteq \mathrm{V}\right)\to \left(\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)\leftrightarrow \forall z\in F\left(x\right)\exists !vv\in \left(F\left(z\right)\cap s\right)\right)$$
77	5 6 76	mp2an	$$⊢\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)\leftrightarrow \forall z\in F\left(x\right)\exists !vv\in \left(F\left(z\right)\cap s\right)$$
78		df-ral	$$⊢\forall z\in F\left(x\right)\exists !vv\in \left(F\left(z\right)\cap s\right)\leftrightarrow \forall z\left(z\in F\left(x\right)\to \exists !vv\in \left(F\left(z\right)\cap s\right)\right)$$
79	77 78	bitri	$$⊢\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)\leftrightarrow \forall z\left(z\in F\left(x\right)\to \exists !vv\in \left(F\left(z\right)\cap s\right)\right)$$
80		fvex	$$⊢F^{-1}\left(s\right)\in \mathrm{V}$$
81	12	a1i	$$⊢y=F^{-1}\left(s\right)\to \left(zRx\leftrightarrow z\in F\left(x\right)\right)$$
82		vex	$$⊢v\in \mathrm{V}$$
83	1 2 82 10	brpermmodel	$$⊢vRz\leftrightarrow v\in F\left(z\right)$$
84	83	a1i	$$⊢y=F^{-1}\left(s\right)\to \left(vRz\leftrightarrow v\in F\left(z\right)\right)$$
85		breq2	$$⊢y=F^{-1}\left(s\right)\to \left(vRy\leftrightarrow vR{F}^{-1}\left(s\right)\right)$$
86		vex	$$⊢s\in \mathrm{V}$$
87	1 2 82 86	brpermmodelcnv	$$⊢vR{F}^{-1}\left(s\right)\leftrightarrow v\in s$$
88	85 87	bitrdi	$$⊢y=F^{-1}\left(s\right)\to \left(vRy\leftrightarrow v\in s\right)$$
89	84 88	anbi12d	$$⊢y=F^{-1}\left(s\right)\to \left(\left(vRz\wedge vRy\right)\leftrightarrow \left(v\in F\left(z\right)\wedge v\in s\right)\right)$$
90	89	bibi1d	$$⊢y=F^{-1}\left(s\right)\to \left(\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\leftrightarrow \left(\left(v\in F\left(z\right)\wedge v\in s\right)\leftrightarrow v=w\right)\right)$$
91	90	albidv	$$⊢y=F^{-1}\left(s\right)\to \left(\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\leftrightarrow \forall v\left(\left(v\in F\left(z\right)\wedge v\in s\right)\leftrightarrow v=w\right)\right)$$
92	91	exbidv	$$⊢y=F^{-1}\left(s\right)\to \left(\exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\leftrightarrow \exists w\forall v\left(\left(v\in F\left(z\right)\wedge v\in s\right)\leftrightarrow v=w\right)\right)$$
93		elin	$$⊢v\in \left(F\left(z\right)\cap s\right)\leftrightarrow \left(v\in F\left(z\right)\wedge v\in s\right)$$
94	93	eubii	$$⊢\exists !vv\in \left(F\left(z\right)\cap s\right)\leftrightarrow \exists !v\left(v\in F\left(z\right)\wedge v\in s\right)$$
95		eu6	$$⊢\exists !v\left(v\in F\left(z\right)\wedge v\in s\right)\leftrightarrow \exists w\forall v\left(\left(v\in F\left(z\right)\wedge v\in s\right)\leftrightarrow v=w\right)$$
96	94 95	bitri	$$⊢\exists !vv\in \left(F\left(z\right)\cap s\right)\leftrightarrow \exists w\forall v\left(\left(v\in F\left(z\right)\wedge v\in s\right)\leftrightarrow v=w\right)$$
97	92 96	bitr4di	$$⊢y=F^{-1}\left(s\right)\to \left(\exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\leftrightarrow \exists !vv\in \left(F\left(z\right)\cap s\right)\right)$$
98	81 97	imbi12d	$$⊢y=F^{-1}\left(s\right)\to \left(\left(zRx\to \exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\right)\leftrightarrow \left(z\in F\left(x\right)\to \exists !vv\in \left(F\left(z\right)\cap s\right)\right)\right)$$
99	98	albidv	$$⊢y=F^{-1}\left(s\right)\to \left(\forall z\left(zRx\to \exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\right)\leftrightarrow \forall z\left(z\in F\left(x\right)\to \exists !vv\in \left(F\left(z\right)\cap s\right)\right)\right)$$
100	80 99	spcev	$$⊢\forall z\left(z\in F\left(x\right)\to \exists !vv\in \left(F\left(z\right)\cap s\right)\right)\to \exists y\forall z\left(zRx\to \exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\right)$$
101	79 100	sylbi	$$⊢\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)\to \exists y\forall z\left(zRx\to \exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\right)$$
102	101	exlimiv	$$⊢\exists s\forall t\in F\left[F\left(x\right)\right]\exists !vv\in \left(t\cap s\right)\to \exists y\forall z\left(zRx\to \exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\right)$$
103	72 102	syl	$$⊢\left(\forall z\left(zRx\to \exists wwRz\right)\wedge \forall z\forall w\left(\left(zRx\wedge wRx\right)\to \left(\neg z=w\to \forall y\left(yRz\to \neg yRw\right)\right)\right)\right)\to \exists y\forall z\left(zRx\to \exists w\forall v\left(\left(vRz\wedge vRy\right)\leftrightarrow v=w\right)\right)$$