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 ∈ D f Fn n ∧ φ ∧ ψ
Assertion bnj900 ⊢ f ∈ B → ∅ ∈ dom ⁡ f

Proof

Step Hyp Ref Expression
1 bnj900.3 ⊢ D = ω ∖ ∅
2 bnj900.4 ⊢ B = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
3 2 bnj1436 ⊢ f ∈ B → ∃ n ∈ D f Fn n ∧ φ ∧ ψ
4 simp1 ⊢ f Fn n ∧ φ ∧ ψ → f Fn n
5 4 reximi ⊢ ∃ n ∈ D f Fn n ∧ φ ∧ ψ → ∃ n ∈ D f Fn n
6 fndm ⊢ f Fn n → dom ⁡ f = n
7 6 reximi ⊢ ∃ n ∈ D f Fn n → ∃ n ∈ D dom ⁡ f = n
8 3 5 7 3syl ⊢ f ∈ B → ∃ n ∈ D dom ⁡ f = n
9 8 bnj1196 ⊢ f ∈ B → ∃ n n ∈ D ∧ dom ⁡ f = n
10 nfre1 ⊢ Ⅎ n ∃ n ∈ D f Fn n ∧ φ ∧ ψ
11 10 nfab ⊢ Ⅎ _ n f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
12 2 11 nfcxfr ⊢ Ⅎ _ n B
13 12 nfcri ⊢ Ⅎ n f ∈ B
14 13 19.37 ⊢ ∃ n f ∈ B → n ∈ D ∧ dom ⁡ f = n ↔ f ∈ B → ∃ n n ∈ D ∧ dom ⁡ f = n
15 9 14 mpbir ⊢ ∃ n f ∈ B → n ∈ D ∧ dom ⁡ f = n
16 nfv ⊢ Ⅎ n ∅ ∈ dom ⁡ f
17 13 16 nfim ⊢ Ⅎ n f ∈ 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 ⊢ ∃ n f ∈ B → n ∈ D ∧ dom ⁡ f = n → f ∈ B → ∅ ∈ dom ⁡ f
24 15 23 ax-mp ⊢ f ∈ B → ∅ ∈ dom ⁡ f