Metamath Proof Explorer

Theorem bnj917

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 bnj917.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
bnj917.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
bnj917.3 ⊢ D = ω ∖ ∅
bnj917.4 ⊢ B = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
bnj917.5 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
Assertion bnj917 ⊢ y ∈ trCl X A R → ∃ f ∃ n ∃ i χ ∧ i ∈ n ∧ y ∈ f ⁡ i

Proof

Step Hyp Ref Expression
1 bnj917.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj917.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj917.3 ⊢ D = ω ∖ ∅
4 bnj917.4 ⊢ B = f | ∃ n ∈ D f Fn n ∧ φ ∧ ψ
5 bnj917.5 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
6 biid ⊢ f Fn n ∧ φ ∧ ψ ↔ f Fn n ∧ φ ∧ ψ
7 1 2 3 4 6 bnj916 ⊢ y ∈ trCl X A R → ∃ f ∃ n ∃ i n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ i ∈ n ∧ y ∈ f ⁡ i
8 bnj252 ⊢ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
9 5 8 bitri ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
10 9 3anbi1i ⊢ χ ∧ i ∈ n ∧ y ∈ f ⁡ i ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ i ∈ n ∧ y ∈ f ⁡ i
11 bnj253 ⊢ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ i ∈ n ∧ y ∈ f ⁡ i ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ i ∈ n ∧ y ∈ f ⁡ i
12 10 11 bitr4i ⊢ χ ∧ i ∈ n ∧ y ∈ f ⁡ i ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ i ∈ n ∧ y ∈ f ⁡ i
13 12 3exbii ⊢ ∃ f ∃ n ∃ i χ ∧ i ∈ n ∧ y ∈ f ⁡ i ↔ ∃ f ∃ n ∃ i n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ i ∈ n ∧ y ∈ f ⁡ i
14 7 13 sylibr ⊢ y ∈ trCl X A R → ∃ f ∃ n ∃ i χ ∧ i ∈ n ∧ y ∈ f ⁡ i