# 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 )`