Metamath Proof Explorer


Theorem bnj594

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 bnj594.1 φ f = pred x A R
bnj594.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj594.3 χ f Fn n φ ψ
bnj594.7 D = ω
bnj594.9 No typesetting found for |- ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) with typecode |-
bnj594.10 No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode |-
bnj594.11 No typesetting found for |- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) with typecode |-
bnj594.15 No typesetting found for |- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
bnj594.16 No typesetting found for |- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) with typecode |-
bnj594.17 τ k n k E j [˙k / j]˙ θ
Assertion bnj594 j n τ θ

Proof

Step Hyp Ref Expression
1 bnj594.1 φ f = pred x A R
2 bnj594.2 ψ i ω suc i n f suc i = y f i pred y A R
3 bnj594.3 χ f Fn n φ ψ
4 bnj594.7 D = ω
5 bnj594.9 Could not format ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) with typecode |-
6 bnj594.10 Could not format ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode |-
7 bnj594.11 Could not format ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) with typecode |-
8 bnj594.15 Could not format ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
9 bnj594.16 Could not format ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) : No typesetting found for |- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) with typecode |-
10 bnj594.17 τ k n k E j [˙k / j]˙ θ
11 3 simp2bi χ φ
12 11 1 sylib χ f = pred x A R
13 7 simp2bi Could not format ( ch' -> ph' ) : No typesetting found for |- ( ch' -> ph' ) with typecode |-
14 13 5 sylib Could not format ( ch' -> ( g ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ch' -> ( g ` (/) ) = _pred ( x , A , R ) ) with typecode |-
15 eqtr3 f = pred x A R g = pred x A R f = g
16 12 14 15 syl2an Could not format ( ( ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) ) : No typesetting found for |- ( ( ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) ) with typecode |-
17 16 3adant1 Could not format ( ( n e. D /\ ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) ) : No typesetting found for |- ( ( n e. D /\ ch /\ ch' ) -> ( f ` (/) ) = ( g ` (/) ) ) with typecode |-
18 fveq2 j = f j = f
19 fveq2 j = g j = g
20 18 19 eqeq12d j = f j = g j f = g
21 17 20 syl5ibr Could not format ( j = (/) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( j = (/) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
22 21 8 sylibr j = θ
23 22 a1d j = j n τ θ
24 bnj253 Could not format ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) ) : No typesetting found for |- ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) ) with typecode |-
25 bnj252 Could not format ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) ) : No typesetting found for |- ( ( n e. D /\ n e. D /\ ch /\ ch' ) <-> ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) ) with typecode |-
26 anidm n D n D n D
27 26 3anbi1i Could not format ( ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) <-> ( n e. D /\ ch /\ ch' ) ) : No typesetting found for |- ( ( ( n e. D /\ n e. D ) /\ ch /\ ch' ) <-> ( n e. D /\ ch /\ ch' ) ) with typecode |-
28 24 25 27 3bitr3i Could not format ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) <-> ( n e. D /\ ch /\ ch' ) ) : No typesetting found for |- ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) <-> ( n e. D /\ ch /\ ch' ) ) with typecode |-
29 df-bnj17 j j n n D τ j j n n D τ
30 10 bnj1095 τ k τ
31 30 bnj1352 j j n n D τ k j j n n D τ
32 29 31 hbxfrbi j j n n D τ k j j n n D τ
33 bnj170 j j n n D j n n D j
34 4 bnj923 n D n ω
35 elnn j n n ω j ω
36 34 35 sylan2 j n n D j ω
37 36 anim1i j n n D j j ω j
38 33 37 sylbi j j n n D j ω j
39 nnsuc j ω j k ω j = suc k
40 rexex k ω j = suc k k j = suc k
41 38 39 40 3syl j j n n D k j = suc k
42 41 bnj721 j j n n D τ k j = suc k
43 32 42 bnj596 j j n n D τ k j j n n D τ j = suc k
44 bnj667 j j n n D τ j n n D τ
45 44 anim1i j j n n D τ j = suc k j n n D τ j = suc k
46 bnj258 j n n D j = suc k τ j n n D τ j = suc k
47 45 46 sylibr j j n n D τ j = suc k j n n D j = suc k τ
48 df-bnj17 j n n D j = suc k τ j n n D j = suc k τ
49 bnj219 j = suc k k E j
50 49 3ad2ant3 j n n D j = suc k k E j
51 50 adantr j n n D j = suc k τ k E j
52 vex k V
53 52 bnj216 j = suc k k j
54 df-3an k j j n n D k j j n n D
55 3anrot k j j n n D j n n D k j
56 ancom k j j n n D n D k j j n
57 54 55 56 3bitr3i j n n D k j n D k j j n
58 eldifi n ω n ω
59 58 4 eleq2s n D n ω
60 nnord n ω Ord n
61 ordtr1 Ord n k j j n k n
62 59 60 61 3syl n D k j j n k n
63 62 imp n D k j j n k n
64 57 63 sylbi j n n D k j k n
65 53 64 syl3an3 j n n D j = suc k k n
66 rsp k n k E j [˙k / j]˙ θ k n k E j [˙k / j]˙ θ
67 10 66 sylbi τ k n k E j [˙k / j]˙ θ
68 65 67 mpan9 j n n D j = suc k τ k E j [˙k / j]˙ θ
69 51 68 mpd j n n D j = suc k τ [˙k / j]˙ θ
70 48 69 sylbi j n n D j = suc k τ [˙k / j]˙ θ
71 70 anim1i Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) ) with typecode |-
72 bnj252 Could not format ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) ) : No typesetting found for |- ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( [. k / j ]. th /\ ( n e. D /\ ch /\ ch' ) ) ) with typecode |-
73 71 72 sylibr Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) ) with typecode |-
74 bnj446 Could not format ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) ) : No typesetting found for |- ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) <-> ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) ) with typecode |-
75 pm3.35 Could not format ( ( ( n e. D /\ ch /\ ch' ) /\ ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) -> ( f ` k ) = ( g ` k ) ) : No typesetting found for |- ( ( ( n e. D /\ ch /\ ch' ) /\ ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) -> ( f ` k ) = ( g ` k ) ) with typecode |-
76 9 75 sylan2b Could not format ( ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) -> ( f ` k ) = ( g ` k ) ) : No typesetting found for |- ( ( ( n e. D /\ ch /\ ch' ) /\ [. k / j ]. th ) -> ( f ` k ) = ( g ` k ) ) with typecode |-
77 74 76 sylbi Could not format ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) : No typesetting found for |- ( ( [. k / j ]. th /\ n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) with typecode |-
78 iuneq1 f k = g k y f k pred y A R = y g k pred y A R
79 73 77 78 3syl Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> U_ y e. ( f ` k ) _pred ( y , A , R ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> U_ y e. ( f ` k ) _pred ( y , A , R ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) with typecode |-
80 bnj658 j n n D j = suc k τ j n n D j = suc k
81 3 simp3bi χ ψ
82 7 simp3bi Could not format ( ch' -> ps' ) : No typesetting found for |- ( ch' -> ps' ) with typecode |-
83 81 82 bnj240 Could not format ( ( n e. D /\ ch /\ ch' ) -> ( ps /\ ps' ) ) : No typesetting found for |- ( ( n e. D /\ ch /\ ch' ) -> ( ps /\ ps' ) ) with typecode |-
84 80 83 anim12i Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) ) with typecode |-
85 simpl Could not format ( ( ps /\ ps' ) -> ps ) : No typesetting found for |- ( ( ps /\ ps' ) -> ps ) with typecode |-
86 85 anim2i Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps ) ) with typecode |-
87 simp3 j n n D j = suc k j = suc k
88 87 anim1i j n n D j = suc k ψ j = suc k ψ
89 simpl1 j n n D j = suc k j = suc k ψ j n
90 df-3an j n n D j = suc k j n n D j = suc k
91 90 biancomi j n n D j = suc k j = suc k j n n D
92 elnn k j j ω k ω
93 53 36 92 syl2an j = suc k j n n D k ω
94 91 93 sylbi j n n D j = suc k k ω
95 2 bnj589 ψ k ω suc k n f suc k = y f k pred y A R
96 95 bnj590 j = suc k ψ k ω j n f j = y f k pred y A R
97 94 96 mpan9 j n n D j = suc k j = suc k ψ j n f j = y f k pred y A R
98 89 97 mpd j n n D j = suc k j = suc k ψ f j = y f k pred y A R
99 88 98 syldan j n n D j = suc k ψ f j = y f k pred y A R
100 84 86 99 3syl Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = U_ y e. ( f ` k ) _pred ( y , A , R ) ) with typecode |-
101 simpr Could not format ( ( ps /\ ps' ) -> ps' ) : No typesetting found for |- ( ( ps /\ ps' ) -> ps' ) with typecode |-
102 101 anim2i Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( ps /\ ps' ) ) -> ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) ) with typecode |-
103 87 anim1i Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( j = suc k /\ ps' ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( j = suc k /\ ps' ) ) with typecode |-
104 simpl1 Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> j e. n ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> j e. n ) with typecode |-
105 6 bnj589 Could not format ( ps' <-> A. k e. _om ( suc k e. n -> ( g ` suc k ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. k e. _om ( suc k e. n -> ( g ` suc k ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) with typecode |-
106 105 bnj590 Could not format ( ( j = suc k /\ ps' ) -> ( k e. _om -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) ) : No typesetting found for |- ( ( j = suc k /\ ps' ) -> ( k e. _om -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) ) with typecode |-
107 94 106 mpan9 Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( j e. n -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) ) with typecode |-
108 104 107 mpd Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ( j = suc k /\ ps' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) with typecode |-
109 103 108 syldan Could not format ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k ) /\ ps' ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) with typecode |-
110 84 102 109 3syl Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( g ` j ) = U_ y e. ( g ` k ) _pred ( y , A , R ) ) with typecode |-
111 79 100 110 3eqtr4d Could not format ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) : No typesetting found for |- ( ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) with typecode |-
112 111 ex Could not format ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( ( j e. n /\ n e. D /\ j = suc k /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
113 47 112 syl Could not format ( ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) /\ j = suc k ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) /\ j = suc k ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
114 43 113 bnj593 Could not format ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( ( j =/= (/) /\ j e. n /\ n e. D /\ ta ) -> E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
115 bnj258 j j n n D τ j j n τ n D
116 19.9v Could not format ( E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( E. k ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
117 114 115 116 3imtr3i Could not format ( ( ( j =/= (/) /\ j e. n /\ ta ) /\ n e. D ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( ( ( j =/= (/) /\ j e. n /\ ta ) /\ n e. D ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
118 117 expimpd Could not format ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
119 28 118 syl5bir Could not format ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( ( j =/= (/) /\ j e. n /\ ta ) -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
120 119 8 sylibr j j n τ θ
121 120 3expib j j n τ θ
122 23 121 pm2.61ine j n τ θ