# 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 𝐷 = ( ω ∖ { ∅ } )
bnj900.4 𝐵 = { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
Assertion bnj900 ( 𝑓𝐵 → ∅ ∈ dom 𝑓 )

### Proof

Step Hyp Ref Expression
1 bnj900.3 𝐷 = ( ω ∖ { ∅ } )
2 bnj900.4 𝐵 = { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
3 2 bnj1436 ( 𝑓𝐵 → ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) )
4 simp1 ( ( 𝑓 Fn 𝑛𝜑𝜓 ) → 𝑓 Fn 𝑛 )
5 4 reximi ( ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) → ∃ 𝑛𝐷 𝑓 Fn 𝑛 )
6 fndm ( 𝑓 Fn 𝑛 → dom 𝑓 = 𝑛 )
7 6 reximi ( ∃ 𝑛𝐷 𝑓 Fn 𝑛 → ∃ 𝑛𝐷 dom 𝑓 = 𝑛 )
8 3 5 7 3syl ( 𝑓𝐵 → ∃ 𝑛𝐷 dom 𝑓 = 𝑛 )
9 8 bnj1196 ( 𝑓𝐵 → ∃ 𝑛 ( 𝑛𝐷 ∧ dom 𝑓 = 𝑛 ) )
10 nfre1 𝑛𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 )
11 10 nfab 𝑛 { 𝑓 ∣ ∃ 𝑛𝐷 ( 𝑓 Fn 𝑛𝜑𝜓 ) }
12 2 11 nfcxfr 𝑛 𝐵
13 12 nfcri 𝑛 𝑓𝐵
14 13 19.37 ( ∃ 𝑛 ( 𝑓𝐵 → ( 𝑛𝐷 ∧ dom 𝑓 = 𝑛 ) ) ↔ ( 𝑓𝐵 → ∃ 𝑛 ( 𝑛𝐷 ∧ dom 𝑓 = 𝑛 ) ) )
15 9 14 mpbir 𝑛 ( 𝑓𝐵 → ( 𝑛𝐷 ∧ dom 𝑓 = 𝑛 ) )
16 nfv 𝑛 ∅ ∈ dom 𝑓
17 13 16 nfim 𝑛 ( 𝑓𝐵 → ∅ ∈ dom 𝑓 )
18 1 bnj529 ( 𝑛𝐷 → ∅ ∈ 𝑛 )
19 eleq2 ( dom 𝑓 = 𝑛 → ( ∅ ∈ dom 𝑓 ↔ ∅ ∈ 𝑛 ) )
20 19 biimparc ( ( ∅ ∈ 𝑛 ∧ dom 𝑓 = 𝑛 ) → ∅ ∈ dom 𝑓 )
21 18 20 sylan ( ( 𝑛𝐷 ∧ dom 𝑓 = 𝑛 ) → ∅ ∈ dom 𝑓 )
22 21 imim2i ( ( 𝑓𝐵 → ( 𝑛𝐷 ∧ dom 𝑓 = 𝑛 ) ) → ( 𝑓𝐵 → ∅ ∈ dom 𝑓 ) )
23 17 22 exlimi ( ∃ 𝑛 ( 𝑓𝐵 → ( 𝑛𝐷 ∧ dom 𝑓 = 𝑛 ) ) → ( 𝑓𝐵 → ∅ ∈ dom 𝑓 ) )
24 15 23 ax-mp ( 𝑓𝐵 → ∅ ∈ dom 𝑓 )