# 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}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
bnj900.4 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
Assertion bnj900 ${⊢}{f}\in {B}\to \varnothing \in \mathrm{dom}{f}$

### Proof

Step Hyp Ref Expression
1 bnj900.3 ${⊢}{D}=\mathrm{\omega }\setminus \left\{\varnothing \right\}$
2 bnj900.4 ${⊢}{B}=\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
3 2 bnj1436 ${⊢}{f}\in {B}\to \exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
4 simp1 ${⊢}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\to {f}Fn{n}$
5 4 reximi ${⊢}\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\to \exists {n}\in {D}\phantom{\rule{.4em}{0ex}}{f}Fn{n}$
6 fndm ${⊢}{f}Fn{n}\to \mathrm{dom}{f}={n}$
7 6 reximi ${⊢}\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}{f}Fn{n}\to \exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}={n}$
8 3 5 7 3syl ${⊢}{f}\in {B}\to \exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\mathrm{dom}{f}={n}$
9 8 bnj1196 ${⊢}{f}\in {B}\to \exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in {D}\wedge \mathrm{dom}{f}={n}\right)$
10 nfre1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)$
11 10 nfab ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left\{{f}|\exists {n}\in {D}\phantom{\rule{.4em}{0ex}}\left({f}Fn{n}\wedge {\phi }\wedge {\psi }\right)\right\}$
12 2 11 nfcxfr ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}$
13 12 nfcri ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{f}\in {B}$
14 13 19.37 ${⊢}\exists {n}\phantom{\rule{.4em}{0ex}}\left({f}\in {B}\to \left({n}\in {D}\wedge \mathrm{dom}{f}={n}\right)\right)↔\left({f}\in {B}\to \exists {n}\phantom{\rule{.4em}{0ex}}\left({n}\in {D}\wedge \mathrm{dom}{f}={n}\right)\right)$
15 9 14 mpbir ${⊢}\exists {n}\phantom{\rule{.4em}{0ex}}\left({f}\in {B}\to \left({n}\in {D}\wedge \mathrm{dom}{f}={n}\right)\right)$
16 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\varnothing \in \mathrm{dom}{f}$
17 13 16 nfim ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({f}\in {B}\to \varnothing \in \mathrm{dom}{f}\right)$
18 1 bnj529 ${⊢}{n}\in {D}\to \varnothing \in {n}$
19 eleq2 ${⊢}\mathrm{dom}{f}={n}\to \left(\varnothing \in \mathrm{dom}{f}↔\varnothing \in {n}\right)$
20 19 biimparc ${⊢}\left(\varnothing \in {n}\wedge \mathrm{dom}{f}={n}\right)\to \varnothing \in \mathrm{dom}{f}$
21 18 20 sylan ${⊢}\left({n}\in {D}\wedge \mathrm{dom}{f}={n}\right)\to \varnothing \in \mathrm{dom}{f}$
22 21 imim2i ${⊢}\left({f}\in {B}\to \left({n}\in {D}\wedge \mathrm{dom}{f}={n}\right)\right)\to \left({f}\in {B}\to \varnothing \in \mathrm{dom}{f}\right)$
23 17 22 exlimi ${⊢}\exists {n}\phantom{\rule{.4em}{0ex}}\left({f}\in {B}\to \left({n}\in {D}\wedge \mathrm{dom}{f}={n}\right)\right)\to \left({f}\in {B}\to \varnothing \in \mathrm{dom}{f}\right)$
24 15 23 ax-mp ${⊢}{f}\in {B}\to \varnothing \in \mathrm{dom}{f}$