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	⊢ 𝐹 = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } )
Assertion	nregmodelf1o	⊢ 𝐹 : V –1-1-onto→ V

Proof

Step	Hyp	Ref	Expression
1		nregmodel.1	⊢ 𝐹 = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } )
2		f1ovi	⊢ I : V –1-1-onto→ V
3		0ex	⊢ ∅ ∈ V
4		snex	⊢ { ∅ } ∈ V
5		f1ofvswap	⊢ ( ( I : V –1-1-onto→ V ∧ ∅ ∈ V ∧ { ∅ } ∈ V ) → ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ , ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ } ) : V –1-1-onto→ V )
6	2 3 4 5	mp3an	⊢ ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ , ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ } ) : V –1-1-onto→ V
7		fvi	⊢ ( { ∅ } ∈ V → ( I ‘ { ∅ } ) = { ∅ } )
8	4 7	ax-mp	⊢ ( I ‘ { ∅ } ) = { ∅ }
9	8	opeq2i	⊢ ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ = ⟨ ∅ , { ∅ } ⟩
10		fvi	⊢ ( ∅ ∈ V → ( I ‘ ∅ ) = ∅ )
11	3 10	ax-mp	⊢ ( I ‘ ∅ ) = ∅
12	11	opeq2i	⊢ ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ = ⟨ { ∅ } , ∅ ⟩
13	9 12	preq12i	⊢ { ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ , ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ } = { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ }
14	13	uneq2i	⊢ ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ , ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ } ) = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } )
15	1 14	eqtr4i	⊢ 𝐹 = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ , ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ } )
16		f1oeq1	⊢ ( 𝐹 = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ , ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ } ) → ( 𝐹 : V –1-1-onto→ V ↔ ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ , ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ } ) : V –1-1-onto→ V ) )
17	15 16	ax-mp	⊢ ( 𝐹 : V –1-1-onto→ V ↔ ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , ( I ‘ { ∅ } ) ⟩ , ⟨ { ∅ } , ( I ‘ ∅ ) ⟩ } ) : V –1-1-onto→ V )
18	6 17	mpbir	⊢ 𝐹 : V –1-1-onto→ V