Theorem nregmodelf1o

Description: Define a permutation F used to produce a model in which ax-reg is false. The permutation swaps (/) and { (/) } and leaves the rest of V fixed. This is an example given after Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 16-Nov-2025)

	Ref	Expression
Hypothesis	nregmodel.1	$$⊢F=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
Assertion	nregmodelf1o	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		nregmodel.1	$$⊢F=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
2		f1ovi	$$⊢\mathrm{I}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
5		f1ofvswap	$$⊢\left(\mathrm{I}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\wedge \varnothing \in \mathrm{V}\wedge \left\{\varnothing \right\}\in \mathrm{V}\right)\to \left(\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩,⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩\right\}\right):\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
6	2 3 4 5	mp3an	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩,⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩\right\}\right):\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
7		fvi	$$⊢\left\{\varnothing \right\}\in \mathrm{V}\to \mathrm{I}\left(\left\{\varnothing \right\}\right)=\left\{\varnothing \right\}$$
8	4 7	ax-mp	$$⊢\mathrm{I}\left(\left\{\varnothing \right\}\right)=\left\{\varnothing \right\}$$
9	8	opeq2i	$$⊢⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩=⟨\varnothing ,\left\{\varnothing \right\}⟩$$
10		fvi	$$⊢\varnothing \in \mathrm{V}\to \mathrm{I}\left(\varnothing \right)=\varnothing$$
11	3 10	ax-mp	$$⊢\mathrm{I}\left(\varnothing \right)=\varnothing$$
12	11	opeq2i	$$⊢⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩=⟨\left\{\varnothing \right\},\varnothing ⟩$$
13	9 12	preq12i	$$⊢\left\{⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩,⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩\right\}=\left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
14	13	uneq2i	$$⊢\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩,⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩\right\}=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
15	1 14	eqtr4i	$$⊢F=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩,⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩\right\}$$
16		f1oeq1	$$⊢F=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩,⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩\right\}\to \left(F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩,⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩\right\}\right):\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\right)$$
17	15 16	ax-mp	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\mathrm{I}\left(\left\{\varnothing \right\}\right)⟩,⟨\left\{\varnothing \right\},\mathrm{I}\left(\varnothing \right)⟩\right\}\right):\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
18	6 17	mpbir	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$