Theorem permaxun

Description: The Axiom of Union ax-un holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 6-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	permaxun	$$⊢\exists y\forall z\left(\exists w\left(zRw\wedge wRx\right)\to zRy\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		fvex	$$⊢F^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\in \mathrm{V}$$
4		breq2	$$⊢y=F^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\to \left(zRy\leftrightarrow zR{F}^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\right)$$
5	4	imbi2d	$$⊢y=F^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\to \left(\left(\exists w\left(zRw\wedge wRx\right)\to zRy\right)\leftrightarrow \left(\exists w\left(zRw\wedge wRx\right)\to zR{F}^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\right)\right)$$
6	5	albidv	$$⊢y=F^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\to \left(\forall z\left(\exists w\left(zRw\wedge wRx\right)\to zRy\right)\leftrightarrow \forall z\left(\exists w\left(zRw\wedge wRx\right)\to zR{F}^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\right)\right)$$
7		vex	$$⊢z\in \mathrm{V}$$
8		vex	$$⊢w\in \mathrm{V}$$
9	1 2 7 8	brpermmodel	$$⊢zRw\leftrightarrow z\in F\left(w\right)$$
10		vex	$$⊢x\in \mathrm{V}$$
11	1 2 8 10	brpermmodel	$$⊢wRx\leftrightarrow w\in F\left(x\right)$$
12		f1ofn	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\to FFn\mathrm{V}$$
13	1 12	ax-mp	$$⊢FFn\mathrm{V}$$
14		ssv	$$⊢F\left(x\right)\subseteq \mathrm{V}$$
15		fnfvima	$$⊢\left(FFn\mathrm{V}\wedge F\left(x\right)\subseteq \mathrm{V}\wedge w\in F\left(x\right)\right)\to F\left(w\right)\in F\left[F\left(x\right)\right]$$
16	13 14 15	mp3an12	$$⊢w\in F\left(x\right)\to F\left(w\right)\in F\left[F\left(x\right)\right]$$
17		elunii	$$⊢\left(z\in F\left(w\right)\wedge F\left(w\right)\in F\left[F\left(x\right)\right]\right)\to z\in \bigcup F\left[F\left(x\right)\right]$$
18	16 17	sylan2	$$⊢\left(z\in F\left(w\right)\wedge w\in F\left(x\right)\right)\to z\in \bigcup F\left[F\left(x\right)\right]$$
19	9 11 18	syl2anb	$$⊢\left(zRw\wedge wRx\right)\to z\in \bigcup F\left[F\left(x\right)\right]$$
20		f1ofun	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\to \mathrm{Fun}F$$
21	1 20	ax-mp	$$⊢\mathrm{Fun}F$$
22		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
23	22	funimaex	$$⊢\mathrm{Fun}F\to F\left[F\left(x\right)\right]\in \mathrm{V}$$
24	21 23	ax-mp	$$⊢F\left[F\left(x\right)\right]\in \mathrm{V}$$
25	24	uniex	$$⊢\bigcup F\left[F\left(x\right)\right]\in \mathrm{V}$$
26	1 2 7 25	brpermmodelcnv	$$⊢zR{F}^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\leftrightarrow z\in \bigcup F\left[F\left(x\right)\right]$$
27	19 26	sylibr	$$⊢\left(zRw\wedge wRx\right)\to zR{F}^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)$$
28	27	exlimiv	$$⊢\exists w\left(zRw\wedge wRx\right)\to zR{F}^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)$$
29	28	ax-gen	$$⊢\forall z\left(\exists w\left(zRw\wedge wRx\right)\to zR{F}^{-1}\left(\bigcup F\left[F\left(x\right)\right]\right)\right)$$
30	3 6 29	ceqsexv2d	$$⊢\exists y\forall z\left(\exists w\left(zRw\wedge wRx\right)\to zRy\right)$$