Metamath Proof Explorer

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 = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } )
Assertion nregmodelf1o 
|- F : _V -1-1-onto-> _V

Proof

Step Hyp Ref Expression
1 nregmodel.1 
 |-  F = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } )
2 f1ovi 
 |-  _I : _V -1-1-onto-> _V
3 0ex 
 |-  (/) e. _V
4 snex 
 |-  { (/) } e. _V
5 f1ofvswap 
 |-  ( ( _I : _V -1-1-onto-> _V /\ (/) e. _V /\ { (/) } e. _V ) -> ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , ( _I ` { (/) } ) >. , <. { (/) } , ( _I ` (/) ) >. } ) : _V -1-1-onto-> _V )
6 2 3 4 5 mp3an 
 |-  ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , ( _I ` { (/) } ) >. , <. { (/) } , ( _I ` (/) ) >. } ) : _V -1-1-onto-> _V
7 fvi 
 |-  ( { (/) } e. _V -> ( _I ` { (/) } ) = { (/) } )
8 4 7 ax-mp 
 |-  ( _I ` { (/) } ) = { (/) }
9 8 opeq2i 
 |-  <. (/) , ( _I ` { (/) } ) >. = <. (/) , { (/) } >.
10 fvi 
 |-  ( (/) e. _V -> ( _I ` (/) ) = (/) )
11 3 10 ax-mp 
 |-  ( _I ` (/) ) = (/)
12 11 opeq2i 
 |-  <. { (/) } , ( _I ` (/) ) >. = <. { (/) } , (/) >.
13 9 12 preq12i 
 |-  { <. (/) , ( _I ` { (/) } ) >. , <. { (/) } , ( _I ` (/) ) >. } = { <. (/) , { (/) } >. , <. { (/) } , (/) >. }
14 13 uneq2i 
 |-  ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , ( _I ` { (/) } ) >. , <. { (/) } , ( _I ` (/) ) >. } ) = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } )
15 1 14 eqtr4i 
 |-  F = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , ( _I ` { (/) } ) >. , <. { (/) } , ( _I ` (/) ) >. } )
16 f1oeq1 
 |-  ( F = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , ( _I ` { (/) } ) >. , <. { (/) } , ( _I ` (/) ) >. } ) -> ( F : _V -1-1-onto-> _V <-> ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , ( _I ` { (/) } ) >. , <. { (/) } , ( _I ` (/) ) >. } ) : _V -1-1-onto-> _V ) )
17 15 16 ax-mp 
 |-  ( F : _V -1-1-onto-> _V <-> ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , ( _I ` { (/) } ) >. , <. { (/) } , ( _I ` (/) ) >. } ) : _V -1-1-onto-> _V )
18 6 17 mpbir 
 |-  F : _V -1-1-onto-> _V