This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj929

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 bnj929.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
bnj929.4 No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
bnj929.7 No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
bnj929.10 ⊢ D = ω ∖ ∅
bnj929.13 ⊢ G = f ∪ n C
bnj929.50 ⊢ C ∈ V
Assertion bnj929 Could not format assertion : No typesetting found for |- ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj929.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj929.4 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
3 bnj929.7 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
4 bnj929.10 ⊢ D = ω ∖ ∅
5 bnj929.13 ⊢ G = f ∪ n C
6 bnj929.50 ⊢ C ∈ V
7 bnj645 ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ → φ
8 bnj334 ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ ↔ f Fn n ∧ n ∈ D ∧ p = suc ⁡ n ∧ φ
9 bnj257 ⊢ f Fn n ∧ n ∈ D ∧ p = suc ⁡ n ∧ φ ↔ f Fn n ∧ n ∈ D ∧ φ ∧ p = suc ⁡ n
10 8 9 bitri ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ ↔ f Fn n ∧ n ∈ D ∧ φ ∧ p = suc ⁡ n
11 bnj345 ⊢ f Fn n ∧ n ∈ D ∧ φ ∧ p = suc ⁡ n ↔ p = suc ⁡ n ∧ f Fn n ∧ n ∈ D ∧ φ
12 bnj253 ⊢ p = suc ⁡ n ∧ f Fn n ∧ n ∈ D ∧ φ ↔ p = suc ⁡ n ∧ f Fn n ∧ n ∈ D ∧ φ
13 10 11 12 3bitri ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ ↔ p = suc ⁡ n ∧ f Fn n ∧ n ∈ D ∧ φ
14 13 simp1bi ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ → p = suc ⁡ n ∧ f Fn n
15 5 6 bnj927 ⊢ p = suc ⁡ n ∧ f Fn n → G Fn p
16 15 fnfund ⊢ p = suc ⁡ n ∧ f Fn n → Fun ⁡ G
17 14 16 syl ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ → Fun ⁡ G
18 5 bnj931 ⊢ f ⊆ G
19 18 a1i ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ → f ⊆ G
20 bnj268 ⊢ n ∈ D ∧ f Fn n ∧ p = suc ⁡ n ∧ φ ↔ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ
21 bnj253 ⊢ n ∈ D ∧ f Fn n ∧ p = suc ⁡ n ∧ φ ↔ n ∈ D ∧ f Fn n ∧ p = suc ⁡ n ∧ φ
22 20 21 bitr3i ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ ↔ n ∈ D ∧ f Fn n ∧ p = suc ⁡ n ∧ φ
23 22 simp1bi ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ → n ∈ D ∧ f Fn n
24 fndm ⊢ f Fn n → dom ⁡ f = n
25 4 bnj529 ⊢ n ∈ D → ∅ ∈ n
26 eleq2 ⊢ dom ⁡ f = n → ∅ ∈ dom ⁡ f ↔ ∅ ∈ n
27 26 biimpar ⊢ dom ⁡ f = n ∧ ∅ ∈ n → ∅ ∈ dom ⁡ f
28 24 25 27 syl2anr ⊢ n ∈ D ∧ f Fn n → ∅ ∈ dom ⁡ f
29 23 28 syl ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ → ∅ ∈ dom ⁡ f
30 17 19 29 bnj1502 ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ → G ⁡ ∅ = f ⁡ ∅
31 5 bnj918 ⊢ G ∈ V
32 1 2 3 31 bnj934 Could not format ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" ) : No typesetting found for |- ( ( ph /\ ( G ` (/) ) = ( f ` (/) ) ) -> ph" ) with typecode |-
33 7 30 32 syl2anc Could not format ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) : No typesetting found for |- ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) with typecode |-