Metamath Proof Explorer

Theorem bnj1133

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 bnj1133.3 ⊢ D = ω ∖ ∅
bnj1133.5 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
bnj1133.7 ⊢ τ ↔ ∀ j ∈ n j E i → [˙j / i]˙ θ
bnj1133.8 ⊢ i ∈ n ∧ τ → θ
Assertion bnj1133 ⊢ χ → ∀ i ∈ n θ

Proof

Step Hyp Ref Expression
1 bnj1133.3 ⊢ D = ω ∖ ∅
2 bnj1133.5 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
3 bnj1133.7 ⊢ τ ↔ ∀ j ∈ n j E i → [˙j / i]˙ θ
4 bnj1133.8 ⊢ i ∈ n ∧ τ → θ
5 1 bnj1071 ⊢ n ∈ D → E Fr n
6 2 5 bnj769 ⊢ χ → E Fr n
7 impexp ⊢ i ∈ n ∧ τ → θ ↔ i ∈ n → τ → θ
8 7 bicomi ⊢ i ∈ n → τ → θ ↔ i ∈ n ∧ τ → θ
9 8 albii ⊢ ∀ i i ∈ n → τ → θ ↔ ∀ i i ∈ n ∧ τ → θ
10 9 4 mpgbir ⊢ ∀ i i ∈ n → τ → θ
11 df-ral ⊢ ∀ i ∈ n τ → θ ↔ ∀ i i ∈ n → τ → θ
12 10 11 mpbir ⊢ ∀ i ∈ n τ → θ
13 vex ⊢ n ∈ V
14 13 3 bnj110 ⊢ E Fr n ∧ ∀ i ∈ n τ → θ → ∀ i ∈ n θ
15 6 12 14 sylancl ⊢ χ → ∀ i ∈ n θ