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 |-