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=ω∖∅
bnj900.4 ⊢B=f|∃n∈DfFnn∧φ∧ψ
Assertion bnj900 ⊢f∈B→∅∈dom⁡f

Proof

Step Hyp Ref Expression
1 bnj900.3 ⊢D=ω∖∅
2 bnj900.4 ⊢B=f|∃n∈DfFnn∧φ∧ψ
3 2 bnj1436 ⊢f∈B→∃n∈DfFnn∧φ∧ψ
4 simp1 ⊢fFnn∧φ∧ψ→fFnn
5 4 reximi ⊢∃n∈DfFnn∧φ∧ψ→∃n∈DfFnn
6 fndm ⊢fFnn→dom⁡f=n
7 6 reximi ⊢∃n∈DfFnn→∃n∈Ddom⁡f=n
8 3 5 7 3syl ⊢f∈B→∃n∈Ddom⁡f=n
9 8 bnj1196 ⊢f∈B→∃nn∈D∧dom⁡f=n
10 nfre1 ⊢Ⅎn∃n∈DfFnn∧φ∧ψ
11 10 nfab ⊢Ⅎ_nf|∃n∈DfFnn∧φ∧ψ
12 2 11 nfcxfr ⊢Ⅎ_nB
13 12 nfcri ⊢Ⅎnf∈B
14 13 19.37 ⊢∃nf∈B→n∈D∧dom⁡f=n↔f∈B→∃nn∈D∧dom⁡f=n
15 9 14 mpbir ⊢∃nf∈B→n∈D∧dom⁡f=n
16 nfv ⊢Ⅎn∅∈dom⁡f
17 13 16 nfim ⊢Ⅎnf∈B→∅∈dom⁡f
18 1 bnj529 ⊢n∈D→∅∈n
19 eleq2 ⊢dom⁡f=n→∅∈dom⁡f↔∅∈n
20 19 biimparc ⊢∅∈n∧dom⁡f=n→∅∈dom⁡f
21 18 20 sylan ⊢n∈D∧dom⁡f=n→∅∈dom⁡f
22 21 imim2i ⊢f∈B→n∈D∧dom⁡f=n→f∈B→∅∈dom⁡f
23 17 22 exlimi ⊢∃nf∈B→n∈D∧dom⁡f=n→f∈B→∅∈dom⁡f
24 15 23 ax-mp ⊢f∈B→∅∈dom⁡f