Metamath Proof Explorer


Theorem bnj570

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 bnj570.3 D = ω
bnj570.17 No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
bnj570.19 η m D n = suc m p ω m = suc p
bnj570.21 ρ i ω suc i n m suc i
bnj570.24 K = y G i pred y A R
bnj570.26 G = f m C
bnj570.40 R FrSe A τ η G Fn n
bnj570.30 No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
Assertion bnj570 R FrSe A τ η ρ G suc i = K

Proof

Step Hyp Ref Expression
1 bnj570.3 D = ω
2 bnj570.17 Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
3 bnj570.19 η m D n = suc m p ω m = suc p
4 bnj570.21 ρ i ω suc i n m suc i
5 bnj570.24 K = y G i pred y A R
6 bnj570.26 G = f m C
7 bnj570.40 R FrSe A τ η G Fn n
8 bnj570.30 Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
9 bnj251 R FrSe A τ η ρ R FrSe A τ η ρ
10 2 simp3bi Could not format ( ta -> ps' ) : No typesetting found for |- ( ta -> ps' ) with typecode |-
11 4 simp1bi ρ i ω
12 11 adantl η ρ i ω
13 3 4 bnj563 η ρ suc i m
14 12 13 jca η ρ i ω suc i m
15 8 bnj946 Could not format ( ps' <-> A. i ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) : No typesetting found for |- ( ps' <-> A. i ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) with typecode |-
16 sp i i ω suc i m f suc i = y f i pred y A R i ω suc i m f suc i = y f i pred y A R
17 15 16 sylbi Could not format ( ps' -> ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) : No typesetting found for |- ( ps' -> ( i e. _om -> ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) ) with typecode |-
18 17 imp32 Could not format ( ( ps' /\ ( i e. _om /\ suc i e. m ) ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ps' /\ ( i e. _om /\ suc i e. m ) ) -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) with typecode |-
19 10 14 18 syl2an τ η ρ f suc i = y f i pred y A R
20 9 19 simplbiim R FrSe A τ η ρ f suc i = y f i pred y A R
21 7 bnj930 R FrSe A τ η Fun G
22 21 bnj721 R FrSe A τ η ρ Fun G
23 6 bnj931 f G
24 23 a1i R FrSe A τ η ρ f G
25 bnj667 R FrSe A τ η ρ τ η ρ
26 2 bnj564 τ dom f = m
27 eleq2 dom f = m suc i dom f suc i m
28 27 biimpar dom f = m suc i m suc i dom f
29 26 13 28 syl2an τ η ρ suc i dom f
30 29 3impb τ η ρ suc i dom f
31 25 30 syl R FrSe A τ η ρ suc i dom f
32 22 24 31 bnj1502 R FrSe A τ η ρ G suc i = f suc i
33 2 simp1bi τ f Fn m
34 bnj252 m D n = suc m p ω m = suc p m D n = suc m p ω m = suc p
35 34 simplbi m D n = suc m p ω m = suc p m D
36 3 35 sylbi η m D
37 eldifi m ω m ω
38 37 1 eleq2s m D m ω
39 nnord m ω Ord m
40 36 38 39 3syl η Ord m
41 40 adantr η ρ Ord m
42 41 13 jca η ρ Ord m suc i m
43 33 42 anim12i τ η ρ f Fn m Ord m suc i m
44 fndm f Fn m dom f = m
45 elelsuc suc i m suc i suc m
46 ordsucelsuc Ord m i m suc i suc m
47 46 biimpar Ord m suc i suc m i m
48 45 47 sylan2 Ord m suc i m i m
49 44 48 anim12i f Fn m Ord m suc i m dom f = m i m
50 eleq2 dom f = m i dom f i m
51 50 biimpar dom f = m i m i dom f
52 43 49 51 3syl τ η ρ i dom f
53 52 3impb τ η ρ i dom f
54 25 53 syl R FrSe A τ η ρ i dom f
55 22 24 54 bnj1502 R FrSe A τ η ρ G i = f i
56 55 iuneq1d R FrSe A τ η ρ y G i pred y A R = y f i pred y A R
57 20 32 56 3eqtr4d R FrSe A τ η ρ G suc i = y G i pred y A R
58 57 5 eqtr4di R FrSe A τ η ρ G suc i = K