This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj900

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj900.3 
|- D = ( _om \ { (/) } )
bnj900.4 
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
Assertion bnj900 
|- ( f e. B -> (/) e. dom f )

Proof

Step Hyp Ref Expression
1 bnj900.3 
 |-  D = ( _om \ { (/) } )
2 bnj900.4 
 |-  B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
3 2 bnj1436 
 |-  ( f e. B -> E. n e. D ( f Fn n /\ ph /\ ps ) )
4 simp1 
 |-  ( ( f Fn n /\ ph /\ ps ) -> f Fn n )
5 4 reximi 
 |-  ( E. n e. D ( f Fn n /\ ph /\ ps ) -> E. n e. D f Fn n )
6 fndm 
 |-  ( f Fn n -> dom f = n )
7 6 reximi 
 |-  ( E. n e. D f Fn n -> E. n e. D dom f = n )
8 3 5 7 3syl 
 |-  ( f e. B -> E. n e. D dom f = n )
9 8 bnj1196 
 |-  ( f e. B -> E. n ( n e. D /\ dom f = n ) )
10 nfre1 
 |-  F/ n E. n e. D ( f Fn n /\ ph /\ ps )
11 10 nfab 
 |-  F/_ n { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
12 2 11 nfcxfr 
 |-  F/_ n B
13 12 nfcri 
 |-  F/ n f e. B
14 13 19.37 
 |-  ( E. n ( f e. B -> ( n e. D /\ dom f = n ) ) <-> ( f e. B -> E. n ( n e. D /\ dom f = n ) ) )
15 9 14 mpbir 
 |-  E. n ( f e. B -> ( n e. D /\ dom f = n ) )
16 nfv 
 |-  F/ n (/) e. dom f
17 13 16 nfim 
 |-  F/ n ( f e. B -> (/) e. dom f )
18 1 bnj529 
 |-  ( n e. D -> (/) e. n )
19 eleq2 
 |-  ( dom f = n -> ( (/) e. dom f <-> (/) e. n ) )
20 19 biimparc 
 |-  ( ( (/) e. n /\ dom f = n ) -> (/) e. dom f )
21 18 20 sylan 
 |-  ( ( n e. D /\ dom f = n ) -> (/) e. dom f )
22 21 imim2i 
 |-  ( ( f e. B -> ( n e. D /\ dom f = n ) ) -> ( f e. B -> (/) e. dom f ) )
23 17 22 exlimi 
 |-  ( E. n ( f e. B -> ( n e. D /\ dom f = n ) ) -> ( f e. B -> (/) e. dom f ) )
24 15 23 ax-mp 
 |-  ( f e. B -> (/) e. dom f )