Metamath Proof Explorer

Theorem nregmodellem

Description: Lemma for nregmodel . (Contributed by Eric Schmidt, 16-Nov-2025)

Ref Expression
Hypotheses nregmodel.1 
|- F = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } )
nregmodel.2 
|- R = ( `' F o. _E )
Assertion nregmodellem 
|- ( x R (/) <-> x e. { (/) } )

Proof

Step Hyp Ref Expression
1 nregmodel.1 
 |-  F = ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } )
2 nregmodel.2 
 |-  R = ( `' F o. _E )
3 1 nregmodelf1o 
 |-  F : _V -1-1-onto-> _V
4 vex 
 |-  x e. _V
5 0ex 
 |-  (/) e. _V
6 3 2 4 5 brpermmodel 
 |-  ( x R (/) <-> x e. ( F ` (/) ) )
7 f1ofun 
 |-  ( F : _V -1-1-onto-> _V -> Fun F )
8 3 7 ax-mp 
 |-  Fun F
9 opex 
 |-  <. (/) , { (/) } >. e. _V
10 9 prid1 
 |-  <. (/) , { (/) } >. e. { <. (/) , { (/) } >. , <. { (/) } , (/) >. }
11 elun2 
 |-  ( <. (/) , { (/) } >. e. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } -> <. (/) , { (/) } >. e. ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } ) )
12 10 11 ax-mp 
 |-  <. (/) , { (/) } >. e. ( ( _I |` ( _V \ { (/) , { (/) } } ) ) u. { <. (/) , { (/) } >. , <. { (/) } , (/) >. } )
13 12 1 eleqtrri 
 |-  <. (/) , { (/) } >. e. F
14 funopfv 
 |-  ( Fun F -> ( <. (/) , { (/) } >. e. F -> ( F ` (/) ) = { (/) } ) )
15 8 13 14 mp2 
 |-  ( F ` (/) ) = { (/) }
16 15 eleq2i 
 |-  ( x e. ( F ` (/) ) <-> x e. { (/) } )
17 6 16 bitri 
 |-  ( x R (/) <-> x e. { (/) } )