Theorem permaxpr

Description: The Axiom of Pairing ax-pr 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	permaxpr	$$⊢\exists z\forall w\left(\left(w=x\vee w=y\right)\to wRz\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(\left\{x,y\right\}\right)\in \mathrm{V}$$
4		breq2	$$⊢z=F^{-1}\left(\left\{x,y\right\}\right)\to \left(wRz\leftrightarrow wR{F}^{-1}\left(\left\{x,y\right\}\right)\right)$$
5	4	imbi2d	$$⊢z=F^{-1}\left(\left\{x,y\right\}\right)\to \left(\left(\left(w=x\vee w=y\right)\to wRz\right)\leftrightarrow \left(\left(w=x\vee w=y\right)\to wR{F}^{-1}\left(\left\{x,y\right\}\right)\right)\right)$$
6	5	albidv	$$⊢z=F^{-1}\left(\left\{x,y\right\}\right)\to \left(\forall w\left(\left(w=x\vee w=y\right)\to wRz\right)\leftrightarrow \forall w\left(\left(w=x\vee w=y\right)\to wR{F}^{-1}\left(\left\{x,y\right\}\right)\right)\right)$$
7		vex	$$⊢w\in \mathrm{V}$$
8		prex	$$⊢\left\{x,y\right\}\in \mathrm{V}$$
9	1 2 7 8	brpermmodelcnv	$$⊢wR{F}^{-1}\left(\left\{x,y\right\}\right)\leftrightarrow w\in \left\{x,y\right\}$$
10	7	elpr	$$⊢w\in \left\{x,y\right\}\leftrightarrow \left(w=x\vee w=y\right)$$
11	9 10	sylbbr	$$⊢\left(w=x\vee w=y\right)\to wR{F}^{-1}\left(\left\{x,y\right\}\right)$$
12	11	ax-gen	$$⊢\forall w\left(\left(w=x\vee w=y\right)\to wR{F}^{-1}\left(\left\{x,y\right\}\right)\right)$$
13	3 6 12	ceqsexv2d	$$⊢\exists z\forall w\left(\left(w=x\vee w=y\right)\to wRz\right)$$