Theorem wfaxpr

Description: The class of well-founded sets models the Axiom of Pairing ax-pr . Part of Corollary II.2.5 of Kunen2 p. 112. (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypothesis	wfax.1	$$⊢W=\bigcup R_1\left[\mathrm{On}\right]$$
Assertion	wfaxpr	$$⊢\forall x\in W\forall y\in W\exists z\in W\forall w\in W\left(\left(w=x\vee w=y\right)\to w\in z\right)$$

Proof

Step	Hyp	Ref	Expression
1		wfax.1	$$⊢W=\bigcup R_1\left[\mathrm{On}\right]$$
2		prwf	$$⊢\left(x\in \bigcup R_1\left[\mathrm{On}\right]\wedge y\in \bigcup R_1\left[\mathrm{On}\right]\right)\to \left\{x,y\right\}\in \bigcup R_1\left[\mathrm{On}\right]$$
3	1	eleq2i	$$⊢x\in W\leftrightarrow x\in \bigcup R_1\left[\mathrm{On}\right]$$
4	1	eleq2i	$$⊢y\in W\leftrightarrow y\in \bigcup R_1\left[\mathrm{On}\right]$$
5	3 4	anbi12i	$$⊢\left(x\in W\wedge y\in W\right)\leftrightarrow \left(x\in \bigcup R_1\left[\mathrm{On}\right]\wedge y\in \bigcup R_1\left[\mathrm{On}\right]\right)$$
6	1	eleq2i	$$⊢\left\{x,y\right\}\in W\leftrightarrow \left\{x,y\right\}\in \bigcup R_1\left[\mathrm{On}\right]$$
7	2 5 6	3imtr4i	$$⊢\left(x\in W\wedge y\in W\right)\to \left\{x,y\right\}\in W$$
8	7	rgen2	$$⊢\forall x\in W\forall y\in W\left\{x,y\right\}\in W$$
9		prclaxpr	$$⊢\forall x\in W\forall y\in W\left\{x,y\right\}\in W\to \forall x\in W\forall y\in W\exists z\in W\forall w\in W\left(\left(w=x\vee w=y\right)\to w\in z\right)$$
10	8 9	ax-mp	$$⊢\forall x\in W\forall y\in W\exists z\in W\forall w\in W\left(\left(w=x\vee w=y\right)\to w\in z\right)$$