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
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj594.2
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj594.3
|- ( ch <-> ( f Fn n /\ ph /\ ps ) )
bnj594.7
|- D = ( _om \ { (/) } )
bnj594.9
|- ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) )
bnj594.10
|- ( ps' <-> A. i e. _om ( suc i e. n -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) )
bnj594.11
|- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) )
bnj594.15
|- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) )
bnj594.16
|- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) )
bnj594.17
|- ( ta <-> A. k e. n ( k _E j -> [. k / j ]. th ) )
Assertion bnj594
|- ( ( j e. n /\ ta ) -> th )

Proof

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