Metamath Proof Explorer

Theorem bnj579

Description: Technical lemma for bnj852 . 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 bnj579.1 ⊢ φ ↔ f ⁡ ∅ = pred x A R
bnj579.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
bnj579.3 ⊢ D = ω ∖ ∅
Assertion bnj579 ⊢ n ∈ D → ∃* f f Fn n ∧ φ ∧ ψ

Proof

Step Hyp Ref Expression
1 bnj579.1 ⊢ φ ↔ f ⁡ ∅ = pred x A R
2 bnj579.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj579.3 ⊢ D = ω ∖ ∅
4 biid ⊢ f Fn n ∧ φ ∧ ψ ↔ f Fn n ∧ φ ∧ ψ
5 biid ⊢ [˙g / f]˙ φ ↔ [˙g / f]˙ φ
6 biid ⊢ [˙g / f]˙ ψ ↔ [˙g / f]˙ ψ
7 biid ⊢ [˙g / f]˙ f Fn n ∧ φ ∧ ψ ↔ [˙g / f]˙ f Fn n ∧ φ ∧ ψ
8 biid ⊢ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ [˙g / f]˙ f Fn n ∧ φ ∧ ψ → f ⁡ j = g ⁡ j ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ [˙g / f]˙ f Fn n ∧ φ ∧ ψ → f ⁡ j = g ⁡ j
9 biid ⊢ ∀ k ∈ n k E j → [˙k / j]˙ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ [˙g / f]˙ f Fn n ∧ φ ∧ ψ → f ⁡ j = g ⁡ j ↔ ∀ k ∈ n k E j → [˙k / j]˙ n ∈ D ∧ f Fn n ∧ φ ∧ ψ ∧ [˙g / f]˙ f Fn n ∧ φ ∧ ψ → f ⁡ j = g ⁡ j
10 1 2 4 5 6 7 3 8 9 bnj580 ⊢ n ∈ D → ∃* f f Fn n ∧ φ ∧ ψ